Proof Systems For First-order Theories
Proof Systems for First-order TheoriesSara NegriUniversity of HelsinkiJoint work with Roy DyckhoffAlgebra and Coalgebra meet Proof Theory,15 - 16 May 2014Queen Mary, University of London1 / 42
OutlineMotivationsRegular theoriesCoherent and geometric theoriesExamplesPropertiesConversion to rulesBeyond geometric theoriesCo-geometric theoriesA problem in formal epistemologyLabelled Calculi for Modal and Intuitionistic LogicsGeneralized geometric ative ExtensionsResultsPrior and Related WorkOpportunities and Challenges2 / 42
MotivationsIBasic goal: maximal extraction of information from the analysis ofproofs in a formal inference systemIAnalytic proof systems for pure logic: sequent calculus, naturaldeductionIExtension to the analysis of mathematical theories:IItheories with universal axioms (N and von Plato 1998)Igeometric theories (N 2003, Simpson 1994 in ND-style)Ia wide class of non-classical logics, including provability logic (N2005), intermediate logics (Dyckhoff and N 2011), temporal logics(Boretti and N 2009), epistemic logics (Hakli and N 2011, 2012)Proof analysis beyond geometric theoriesIIGeneralized geometric implications – Sahlqvist fragment (N 2014),knowability logic (Maffezioli, Naibo and N 2013), conditional logics(N and Sbardolini 2014), .Arbitrary first-order theories/frame conditions?3 / 42
Design principles and propertiesConversion of axioms into rules of inference is obtained by a uniformprocedure that has to respect the properties of the logical calculus towhich the rules are added.Natural deduction with general elimination rules or better sequentcalculus.Sequent calculus as a ground logical calculus abductive tool to findthe rules; invertibility key feature4 / 42
1. Regular extensionsTake the classical Gentzen-Ketonen-Kleene contraction- and cut-freecalculus G3c and rules that correspond to axiomsP1 & . . . &Pm Q1 · · · Qnformulation as a left rule:Q1 , Γ . . . Qn , Γ RP1 , . . . , Pm , Γ, formulation as a right rule:Γ , P1 . . . Γ , PmRΓ, , Q1 , . . . , Qn5 / 42
Cut eliminationThe reason why we get full cut elimination lies in the form of the rules:- the rules act on only one side of sequents- the rules act on atomic formulasWe have, say,.RΓ , P P, Γ0 0CutΓ, Γ0 , 0If R is a left rule with P principal, P is not principal in the left premissof cut and cut can be permuted6 / 42
Coherent and geometric implicationsA formula is Horn iff built from atoms (and ) using only .A formula is coherent, aka “positive”, iff built from atoms (and , )using only , and .A formula is geometric iff built from atoms (and , ) using only , , and infinitary disjunctions.A sentence is a coherent implication iff of the form x.C D, whereC, D are coherent [degenerate case with as C left unwritten]A sentence is a geometric implication iff of the form x.C D, whereC, D are geometric.Theorem: Any coherent sentence is equivalent to a finite conjunctionof sentences of the form x.C D where C is Horn and D is a (finite)disjunction of existentially quantified Horn formulae.Theorem: Any geometric sentence is equivalent to a (possiblyinfinite) conjunction of sentences of the form x.C D where C isHorn and D is a (possibly infinite) disjunction of existentiallyquantified Horn formulae.7 / 42
ExamplesUniversal formulae x.A can be written as finite conjunctions ofcoherent implications, just by putting A into CNF, distributing past and rewriting (e.g. P Q as P Q). (No is involved. and maybe useful.)Theory of local rings is axiomatised by coherent implications,including x y (xy 1) y ((1 x)y 1)Theory of transitive relations is axiomatised by coherent implication: xyz.(Rxy Ryz) Rxz.Theory of partial order is axiomatised by coherent implications,including: xy . (x y y x) x yTheory of strongly directed relations is axiomatised by coherentimplication: xyz.(Rxy Rxz) u.Ryu Rzu(Infinitary) theory of torsion abelian groupsis axiomatised byWgeometric implications, including x. n 1 (nx 0)8 / 42
Other examplesObs.: Reformulation of the axioms and/or choice of basic conceptsmay be crucial for obtaining a geometric axiomatization.Fields: a 0 y a · y 1 is not geometric, but the equivalenta 0 y a · y 1 is.Robinson arithmetic: a 0 y a s(y ) is not geometric, but theequivalent a 0 y a s(y ) isReal-closed fields: a2n 1 0 y a2n 1 · y 2n 1 a2n · y 2n . . . a1 · y a0 0 is notgeometric, but the equivalenta2n 1 0 y a2n 1 · y 2n 1 a2n · y 2n . . . a1 · y a0 0 is.Classical projective geometry: Not a geometric theory!Axiom of existence of three non-collinear points. x y z( x y & z ln(x, y ))if the basic notions are replaced by the constructive notions ofapartness between points and lines and “outsideness” of a point froma line, a geometric axiomatization is found: x y z(x 6 y & z / ln(x, y ))9 / 42
Properties of coherent theoriesFor the time being we ignore infinitary theories: so we will just discusscoherence. “Geometric” is often used synonymously with “coherent”,and vice versa.“Barr’s Theorem”: Coherent implications form a “Glivenko Class”, i.e.if a sequent I1 , . . . , In I0 is provable classically, then it can beproved intuitionistically, provided each Ii is a coherent implication.Coherent theories (i.e. those axiomatised by coherent implications)are preserved by pullback along geometric morphisms between topoi.Coherent theories are those whose class of models is closed underdirected limits.Coherent theories are “exactly the theories expressible by naturaldeduction rules in a certain simple form in which only atomic formulasplay a critical part” (Simpson 1994).Coherent implications can be converted directly to inference rules insuch a fashion that admissibility of the structural rules of theunderlying calculus is unaffected (Negri 2003).10 / 42
Conversion of coherent implications to rules: ExampleIThe coherent implication xyz.(x y y z) (y x z y ) isconverted to the inference ruley x, x y , y z, Γ z y , x y , y z, Γ x y , y z, Γ (If is a partial order, this says that the depth is at most 2.)IThe coherent implication xyz.(x y x z) w(y w z w) is converted to theinference rule (in which w is fresh, i.e. not in the conclusion):y w, z w, x y , x z, Γ x y , x z, Γ (If is a partial order, this says that it is “strongly directed”.)11 / 42
Conversion, in generalUse a canonical form for geometric implications: they are equivalentto conjunctions of formulas x(P1 & . . . &Pm y 1 M1 · · · y n Mn )Pi atomicV formulaMi j Qij conjunction of atomic formulasnone of the variables in y j are free in Pi .each is converted to a rule of the formQ 1 (z 1 /y 1 ), P, Γ .Q n (z n /y n ), P, Γ P, Γ GRS- The eigenvariables zi must not be free in P, Γ, .12 / 42
Coherent/geometric theories are not enoughIAxiom of non-collinearity of classical projective and affinegeometry x y z( x y & z ln(x, y ))IAxiom of existence of a least upper bound xy z((x 6 z & y 6 z) & w(x 6 w & y 6 w z 6 w))are not geometric implications.13 / 42
Co-geometric theories- a formula is co-geometric if it does not contain or .- a co-geometric implication has the form, with A and B co-geometricformulas, x . . . z(A B)- canonical form: conjunctions of x( y1 M1 & . . . & yn Mn P1 · · · Pm )with the Mi disjunctions of atoms- classical projective and affine geometries with the axiom ofnon-collinearity are co-geometric: write non-collinearity as x y z(x y z ln(x, y ))Γ , x y , z ln(x, y )Non-collΓ (x, y , z not free in the conclusion)14 / 42
Co-geometric theoriesFormulate right rules as mirror images of geometric rules:Γ , P11 , . . . , P1k . . . Γ , Pm1 , . . . , PmlΓ, , Q1 , . . . , Qn ,RThe Pi can contain eigenvariablesBasic proof-theoretical results go through as for geometric rulesThe duality between geometric and co-geometric theories used forchanging the primitive notions in the sequent formulation of a theory.Meta-theoretical results imported from one theory to its dual byexploiting the symmetry of their associated sequent calculi.Herbrand’s theorem for geometric and co-geometric theories (N andvon Plato 2011).15 / 42
A motivating problem: Knowability logicEpistemic conceptions of truth justify the knowability principle:If A is true, then it is possible to know that AA 3KA (KP)The Church-Fitch paradox (1945–1962): formal derivation from theknowability principle to (collective) omniscience:All truths are actually knownA KA (OP)The main goal has been to show that the paradox does not affect anintuitionistic conception of truth.The derivation of the paradox is indeed done in classical logic.Intuitionistic logic proves its negative version, but to prove intuitionisticunderivability of the positive version, a careful proof analysis isneeded.16 / 42
Knowability logicIntuitionistic logic blocks the derivation of OP from theMoore-instance (A& KA) of KP. Is this enough? No!So the goal has been to develop a proof theory for knowability logic: acut-free sequent system for bimodal logic extended by the knowabilityprinciple.The knowability principle does not reduce to atomic instances, so itcannot be translated into rules through the methodology of “axiomsas rules”.Something similar can be done.17 / 42
Labelled Calculi for Modal and Intuitionistic LogicsLabelled sequent calculi obtained by the internalization of Kripkesemantics (Negri 2005)Something similar (Dyckhoff & Negri 2012) can be done forintuitionistic logic, with special rules for implication using a partialorder (including reflexivity and transitivity) as the accessibilityrelation.Rules for implication are then:x y , x : A B, Γ y : A, x y , x : A B, y : B, Γ L x y , x : A B, Γ and, with y fresh,x y , y : A, Γ y : B, R Γ x : A B, 18 / 42
A labelled calculus for knowability logicExtend the intuitionistic labelled calculus by rules for K and 3:IxKA iff for all y , xRK y implies yAIx3A iff for some y , xR3 y and yAThe clauses are converted into rules:y : A, x : KA, xRK y , Γ x : KA, xRK y , Γ xR3 y , y : A, Γ x : 3A, Γ L3LKxRK y , Γ , y : AΓ , x : KARKxR3 y , Γ , x : 3A, y : AxR3 y , Γ , x : 3AR3In RK and L3, y does not appear in Γ and 19 / 42
From (modal) axioms to (frame) rulesRecall that various extensions are obtained by adding the frameproperties that correspond to the added axioms, for exampleLogicAxiomFrame propertyT2A A x xRx reflexivity42A 22A xyz(xRy & yRz xRz) trans.E3A 23A xyz(xRy & xRz yRz) euclid.BA 23A xy (xRy yRx) symmetryD2A 3A x y xRy seriality2W32A 23A2(2A A) 2A xyz(xRy & xRz w(yRw & zRw))trans., irref., and no infinite R-chainsRulexRx, Γ Γ xRz, Γ xRy , yRz, Γ yRz, Γ xRy , xRz, Γ yRx, Γ xRy , Γ xRy , Γ yΓ yRw, zRw, Γ xRy , xRz, Γ wmodified 2 rulesbut knowability is different from all such cases.20 / 42
Finding the right rules for knowability logicThe calculus itself is used to find the frame condition and the rulesneeded, by root-first proof search: x : A 3KA21 / 42
Finding the right rules for knowability logicThe calculus itself is used to find the frame condition and the rulesneeded, by root-first proof search:x 6 y , y : A y : 3KA x : A 3KAR 22 / 42
Finding the right rules for knowability logicThe calculus itself is used to find the frame condition and the rulesneeded, by root-first proof search:x 6 y , yR3 z, y : A y : 3KASer3x 6 y , y : A y : 3KAR x : A 3KA23 / 42
Finding the right rules for knowability logicThe calculus itself is used to find the frame condition and the rulesneeded, by root-first proof search:x 6 y , yR3 z, y : A y : 3KA, z : KAR3x 6 y , yR3 z, y : A y : 3KASer3x 6 y , y : A y : 3KAR x : A 3KA24 / 42
Finding the right rules for knowability logicThe calculus itself is used to find the frame condition and the rulesneeded, by root-first proof search:x 6 y , yR3 z, zRK w, y : A y : 3KA, w : ARKx 6 y , yR3 z, y : A y : 3KA, z : KAR3x 6 y , yR3 z, y : A y : 3KASer3x 6 y , y : A y : 3KAR x : A 3KA25 / 42
Finding the right rules for knowability logicThe calculus itself is used to find the frame conditions and the rulesneeded, by root-first proof search:x 6 y , y 6 w, yR3 z, zRK w, y : A y : 3KA, w : A3K-Trx 6 y , yR3 z, zRK w, y : A y : 3KA, w : ARKx 6 y , yR3 z, y : A y : 3KA, z : KAR3x 6 y , yR3 z, y : A y : 3KASer3x 6 y , y : A y : 3KAR x : A 3KAthe uppermost sequent is derivable by monotonicity.26 / 42
Finding the right rules for knowability logic (cont.)The two extra-logical rules used are:xR3 y , Γ Γ Ser3x 6 z, xR3 y , yRK z, Γ xR3 y , yRK z, Γ 3K-TrSer3 has the condition y / Γ, . The rules correspond to the frameproperties x y .xR3 ySer3 x y z(xR3 y & yRK z x 6 z)3K-TrThe universal frame property 3K-Tr is, however, too strong: Theinstance of rule 3K-Tr used in the derivation of KP is not applied(root first) to an arbitrary sequent, but to one in which the middle termis the eigenvariable introduced by Ser3 .So we have the requirements:I3K-Tr has to be applied above Ser3IThe middle term of 3K-Tr is the eigenvariable of Ser3 .27 / 42
Finding the right rules for knowability logic (cont.)The system of rules is equivalent to the frame property x y (xR3 y & z(yRK z x 6 z))KP-FrThe system with rules 3K-Tr and Ser3 that respect the side conditionis a cut-free equivalent of the system that employs KP-Fr as anaxiomatic sequent in addition to the structural rules.The rules that correspond to KP-Fr do not follow the geometric rulescheme. However, all the structural rules are still admissible in thepresence of such rules.The system obtained by the addition of suitable combinations ofthese two rules provides a complete contraction- and cut-free systemfor the knowability logic G3KP, that is, intuitionistic bimodal logicextended with KP.Intuitionistic solution to Fitch’s paradox through an exhaustive proofanalysis in KP: OP is not derivable in G3KP.cf. Maffezioli, Naibo, and N (2012).28 / 42
3. Generalizing geometric implications(Negri 2013)Normal form for geometric implications: x(&Pi y1 M1 · · · yn Mn )GAPi atomic formulas, Mj conjunctions of atomic formulasQj1 & . . . & Qjkj , yj not free in the Pi .Geometric implications are taken as the base case in the inductivedefinition of generalized geometric implications.GA0 GAGRS0 GRSGA1 x( & Pi y1 & GA0 · · · ym & GA0 )GAn 1 x( & Pi y1 & GAn · · · ym & GAn )here & GAi denotes a conjunction of GAi -axioms.29 / 42
ExamplesIFrame condition for the knowability principle, A 3KA is x y (xR3 y & z(yRK z x 6 z)) and corresponds to the systemof rules xR3 y , Γ Ser3 (y fresh) Γ x 6 z, xR3 y , yRK z, Γ xR3 y , yRK z, Γ II3K-TrContinuity axiom δ x(x B(δ) f (x) B( )) is in GA1 .The class GA1 does not require the presence of quantifiers:(P Q) (Q P) is in GA1 (a degenerate case withoutvariables).The system of rules has the formQ, P, Γ0 0 P, Q, Γ00 00P, Γ0 0Q, Γ00 00.Γ Γ Γ 30 / 42
The Sahlqvist fragmentIConversion into systems of rules works in full generality for theclass of generalized geometric implicationsIgives operative characterisation in terms of Glivenko classes:generalised geometric implication no negative , IKracht formulas (frame correspondents of Sahlqvist formulas)belong to the same classIthus conversion of g.g.i. into rules gives proof systems for all theSahlqvist fragment31 / 42
Other motivations, and another solution(Dyckhoff and Negri 2014)Not all theories are axiomatised by geometric implications, e.g.IThe “McKinsey condition” (a frame condition for modal logic,related to the McKinsey axiom 23A 32A) x y . xRy ( z. yRz y z)is not a coherent implication.IThe “strict seriality condition” x. y . xRy (yRx)are not geometric implications; they are are generalised geometricimplications; such theories can be treated as systems of rules BUT:ISystems of rules are non-local, require bookkeeping of thedependence of eigenvariablesINot all first-order axioms are generalised geometric implications,e.g. xyx(xRy &yRz xRz) v ( vRv )32 / 42
SolutionsThe technique we adopt is called “atomisation”, and was introducedby Skolem (1920) (in his proofs of Löwenheim’s theorems). Alsocalled “Morleyization”.IIntroduce a new unary predicate symbol M (for Maximal), andreplace the McKinsey condition x y . xRy ( z.yRz y z)by two geometric implications: x( y . xRy M(y )) yz(M(y ) yRz y z)IIntroduce a new binary predicate symbol S, and replace the strictseriality condition x. y . xRy (yRx) by two geometricimplications: x y .xRy ySx xy (xRy xSy )What is going on here ?33 / 42
Conservative and Skolem ExtensionsLet T be a theory in a language L and L0 be a language extending L.A theory T 0 in L0 is a conservative extension of T iff (i) every theoremof T is a theorem of T 0 and (ii) every theorem of T 0 expressed in L isa theorem of T .So, rather than proving theorems (expressed in L) in T it suffices toprove them in T 0 , where it may be easier.A related condition is that of being a “Skolem extension”. T 0 is aSkolem extension of T iff (i) every theorem of T is a theorem of T 0and (ii) for some substitution of L-formulae for predicate symbols notin L, every theorem of T 0 becomes a theorem of T .34 / 42
ResultsTheorem If T 0 is a Skolem extension of T , then (i) it is a conservativeextension and (ii) they are satisfiable in the same domains.Proof Routine.Theorem Every first-order axiomatic theory has a Skolem extensionaxiomatised by coherent implications.Proof Generalisation of the two tricks given above: one can replaceeach axiom by its prenex normal form, with the body in DNF, and useone technique to strip off pairs x y of quantifiers and the othertechnique to get rid of negated atoms. New predicate symbols areintroduced, along with coherent implications that (partially) expresstheir meanings.Corollary Every first-order axiomatic theory has a conservativeextension axiomatised by coherent implications.Corollary Every first-order axiomatic theory has an -extension withmodels in the same domains.Remark This corollary is the result proved by Skolem 1920, as ameans to simplify the proofs of Löwenheim’s theorems aboutcardinality of models.35 / 42
A view through rulesTranslation into rulesIGives an alternative (simpler) proof of the conservativity resultIDefines the rule system equivalent to the given first-order theoryIExtends the labelled approach to arbitrary first-order frameconditions36 / 42
Labelled Calculi for Intermediate LogicsIntermediate (aka “superintuitionistic”) logics are those, e.g.Gödel-Dummett logic and Jankov-De Morgan logic, betweenintuitionistic and classical logic.They can usually be presented using some “frame conditions”, e.g. xy . (x y ) (y x) for G-D logic; so we need to incorporate suchconditions into the rules of the sequent calculus.Where (as here) the condition is coherent, this is easy (and we canrestrict to cases where x and y are in the conclusion):x y , Γ y x, Γ Γ and we also need reflexivity (for x in the conclusion) and transitivity:x x, Γ ReflΓ x z, x y , y z, Γ Transx y , y z, Γ .37 / 42
Labelled Calculi for Intermediate Logics 2Not all frame conditions are coherent. E.g., (i) the McKinsey condition(in modal logic) above and (ii) that for the Kreisel-Putnam(intermediate) logic, axiomatised by( A (B C)) (( A B) ( A C)).The condition is xyz. (x y x z) (y z z y u.(x u u y u z F (u, y , z)))where F (u, y , z) abbreviates v . u v w. (v w
Motivations I Basic goal: maximal extraction of information from the analysis of proofs in a formal inference system I Analytic proof systems for pure logic: sequent calculus, natural deduction I Extension to the analysis of mathematical theories: I theories with universal axioms (N and von Plato 1998) I geometric theories (N 2003, Simpson 1994 in ND-style) I a wide class of non-classical .
since 1950 E. German, Suhl choke-bore barrel mark PROOF MARKS: GERMAN PROOF MARKS, cont. PROOF MARKS: ITALIAN PROOF MARKS, cont. ITALIAN PROOF MARKS PrOOF mark CirCa PrOOF hOuse tYPe OF PrOOF and gun since 1951 Brescia provisional proof for all guns since 1951 Gardone provisional proof for all guns
PROOF MARKS: BELGIAN PROOF MARKSPROOF MARKS: BELGIAN PROOF MARKS, cont. BELGIAN PROOF MARKS PrOOF mark CirCa PrOOF hOuse tYPe OF PrOOF and gun since 1852 Liege provisional black powder proof for breech loading guns and rifled barrels - Liege- double proof marking for unfurnished barrels - Liege- triple proof provisional marking for
Bruksanvisning för bilstereo . Bruksanvisning for bilstereo . Instrukcja obsługi samochodowego odtwarzacza stereo . Operating Instructions for Car Stereo . 610-104 . SV . Bruksanvisning i original
2154 PROOF MARKS: GERMAN PROOF MARKS, cont. PROOF MARK CIRCA PROOF HOUSE TYPE OF PROOF AND GUN since 1950 E. German, Suhl repair proof since 1950 E. German, Suhl 1st black powder proof for smooth bored barrels since 1950 E. German, Suhl inspection mark since 1950 E. German, Suhl choke-bore barrel mark PROOF MARKS: GERMAN PROOF MARKS, cont.
PROOF MARKS: GERMAN PROOF MARKSPROOF MARKS: GERMAN PROOF MARKS, cont. GERMAN PROOF MARKS Research continues for the inclusion of Pre-1950 German Proofmarks. PrOOF mark CirCa PrOOF hOuse tYPe OF PrOOF and gun since 1952 Ulm since 1968 Hannover since 1968 Kiel (W. German) since 1968 Munich since 1968 Cologne (W. German) since 1968 Berlin (W. German)
10 tips och tricks för att lyckas med ert sap-projekt 20 SAPSANYTT 2/2015 De flesta projektledare känner säkert till Cobb’s paradox. Martin Cobb verkade som CIO för sekretariatet för Treasury Board of Canada 1995 då han ställde frågan
service i Norge och Finland drivs inom ramen för ett enskilt företag (NRK. 1 och Yleisradio), fin ns det i Sverige tre: Ett för tv (Sveriges Television , SVT ), ett för radio (Sveriges Radio , SR ) och ett för utbildnings program (Sveriges Utbildningsradio, UR, vilket till följd av sin begränsade storlek inte återfinns bland de 25 största
Hotell För hotell anges de tre klasserna A/B, C och D. Det betyder att den "normala" standarden C är acceptabel men att motiven för en högre standard är starka. Ljudklass C motsvarar de tidigare normkraven för hotell, ljudklass A/B motsvarar kraven för moderna hotell med hög standard och ljudklass D kan användas vid
