01150nas a2200133 4500008004100000245006000041210006000101260001900161300001200180490000800192520074100200100002400941856005100965 2015 eng d00aApplicative theories for logarithmic complexity classes0 aApplicative theories for logarithmic complexity classes bElseviercJune a115-1350 v5853 aWe present applicative theories of words corresponding to weak, and especially logarithmic, complexity classes. The theories for the logarithmic hierarchy and alternating logarithmic time formalise function algebras with concatenation recursion as main principle. We present two theories for logarithmic space where the first formalises a new two-sorted algebra which is very similar to Cook and Bellantoni's famous two-sorted algebra B for polynomial time [4]. The second theory describes logarithmic space by formalising concatenation- and sharply bounded recursion. All theories contain the predicates WW representing words, and VV representing temporary inaccessible words. They are inspired by Cantini's theories [6] formalising B.1 aEberhard, Sebastian uhttp://www.iam.unibe.ch/ltgpub/2015/ebat15.pdf02228nas a2200193 4500008004100000245004900041210004900090260003600139300001200175490000700187520164800194100002401842700001901866700002501885700001901910700003301929700002201962856005001984 2015 eng d00aUnfolding Feasible Arithmetic and Weak Truth0 aUnfolding Feasible Arithmetic and Weak Truth aDordrechtbSpringer Netherlands a153-1670 v363 aIn this paper we continue Feferman?s unfolding program initiated in (Feferman, vol. 6 of Lecture Notes in Logic, 1996) which uses the concept of the unfolding U(S) of a schematic system S in order to describe those operations, predicates and principles concerning them, which are implicit in the acceptance of S. The program has been carried through for a schematic system of non-finitist arithmetic NFA in Feferman and Strahm (Ann Pure Appl Log, 104(1?3):75?96, 2000) and for a system FA (with and without Bar rule) in Feferman and Strahm (Rev Symb Log, 3(4):665?689, 2010). The present contribution elucidates the concept of unfolding for a basic schematic system FEA of feasible arithmetic. Apart from the operational unfolding U0(FEA) of FEA, we study two full unfolding notions, namely the predicate unfolding U(FEA) and a more general truth unfolding UT(FEA) of FEA, the latter making use of a truth predicate added to the language of the operational unfolding. The main results obtained are that the provably convergent functions on binary words for all three unfolding systems are precisely those being computable in polynomial time. The upper bound computations make essential use of a specific theory of truth TPT over combinatory logic, which has recently been introduced in Eberhard and Strahm (Bull Symb Log, 18(3):474?475, 2012) and Eberhard (A feasible theory of truth over combinatory logic, 2014) and whose involved proof-theoretic analysis is due to Eberhard (A feasible theory of truth over combinatory logic, 2014). The results of this paper were first announced in (Eberhard and Strahm, Bull Symb Log 18(3):474?475, 2012).1 aEberhard, Sebastian1 aStrahm, Thomas1 aAchourioti, Theodora1 aGalinon, Henri1 aFernández, José, Martínez1 aFujimoto, Kentaro uhttp://www.iam.unibe.ch/ltgpub/2015/esu15.pdf00417nas a2200133 4500008004100000022001400041245005600055210005600111300001400167490000800181653001900189100002400208856005100232 2014 eng d a0168-007200aA feasible theory of truth over combinatory algebra0 aA feasible theory of truth over combinatory algebra a1009-10330 v16510aTruth theories1 aEberhard, Sebastian uhttp://www.iam.unibe.ch/ltgpub/2012/ebe12a.pdf00419nas a2200097 4500008004100000245006700041210006500108260007400173100002400247856005000271 2013 eng d00aWeak applicative theories, truth, and computational complexity0 aWeak applicative theories truth and computational complexity aInstitut für Informatik und angewandte MathematikbUniversität Bern1 aEberhard, Sebastian uhttp://www.iam.unibe.ch/ltgpub/2013/ebe13.pdf00520nas a2200169 4500008004100000245005200041210005200093260001700145300001200162100002400174700001900198700001900217700001900236700002000255700002500275856005000300 2012 eng d00aWeak theories of truth and explicit mathematics0 aWeak theories of truth and explicit mathematics bOntos Verlag a157-1841 aEberhard, Sebastian1 aStrahm, Thomas1 aBerger, Ulrich1 aDiener, Hannes1 aSchuster, Peter1 aSeisenberger, Monika uhttp://www.iam.unibe.ch/ltgpub/2012/es12a.pdf00419nas a2200097 4500008004100000245006600041210006600107260007400173100002400247856005000271 2009 eng d00aAspekte beweisbar totaler Funktionen in applikativen Theorien0 aAspekte beweisbar totaler Funktionen in applikativen Theorien aInstitut für Informatik und angewandte MathematikbUniversität Bern1 aEberhard, Sebastian uhttp://www.iam.unibe.ch/ltgpub/2009/ebe09.pdf