Sep 25, 2013 - computer checking of such discourse in full detail, and collection of .... Our software system ingests pr
Proof verification within set theory Eugenio G. Omodeo
Dip. Matematica e Geoscienze — DMI
CILC’13, Catania, 25/09/2013
Eugenio G. Omodeo
Proof verification within set theory
1/26
Kurt Gödel
( 1906–1978 )
The development of mathematics towards greater precision has led, as is well known, to the formalization of large domains of it, so that one can prove any theorem using nothing but a few mechanical rules. ( 1931 )
Either mathematics is too big for the human mind or the human mind is more than a machine. Eugenio G. Omodeo
Proof verification within set theory
2/26
Kurt Gödel
( 1906–1978 )
The development of mathematics towards greater precision has led, as is well known, to the formalization of large domains of it, so that one can prove any theorem using nothing but a few mechanical rules. ( 1931 )
Either mathematics is too big for the human mind or the human mind is more than a machine. Eugenio G. Omodeo
Proof verification within set theory
2/26
Visionaries’ dream becomes proof technology
A Proof verifier is an interactive program for manipulation of the state of a mathematical discourse. It allows computer checking of such discourse in full detail, and collection of the resulting theorems for subsequent re-use. It must Besides their theoretical interest, proof verifiers have one potential practical use: Program Verification.
Eugenio G. Omodeo
Proof verification within set theory
3/26
Visionaries’ dream becomes proof technology
A Proof verifier is an interactive program for manipulation of the state of a mathematical discourse. It allows computer checking of such discourse in full detail, and collection of the resulting theorems for subsequent re-use. It must Besides their theoretical interest, proof verifiers have one potential practical use: Program Verification.
Eugenio G. Omodeo
Proof verification within set theory
3/26
Visionaries’ dream becomes proof technology
A Proof verifier is an interactive program for manipulation of the state of a mathematical discourse. It allows computer checking of such discourse in full detail, and collection of the resulting theorems for subsequent re-use. It must 1
2
only allow theorems to be derived ; allow all theorems to be derived .
Besides their theoretical interest, proof verifiers have one potential practical use: Program Verification.
Eugenio G. Omodeo
Proof verification within set theory
3/26
Visionaries’ dream becomes proof technology
A Proof verifier is an interactive program for manipulation of the state of a mathematical discourse. It allows computer checking of such discourse in full detail, and collection of the resulting theorems for subsequent re-use. It must 1
2
only allow theorems to be derived ; allow all theorems to be derived .
Besides their theoretical interest, proof verifiers have one potential practical use: Program Verification.
Eugenio G. Omodeo
Proof verification within set theory
3/26
Visionaries’ dream becomes proof technology A Proof verifier is an interactive program for manipulation of the state of a mathematical discourse. It allows computer checking of such discourse in full detail, and collection of the resulting theorems for subsequent re-use. It must 1
2
only allow theorems to be derived ; allow all theorems to be derived .
Besides their theoretical interest, proof verifiers have one potential practical use: Program Verification. J. T. Schwartz, D. Cantone, and E. G. Omodeo. Computational Logic and Set Theory. Applying analysis. Springer-Verlag, 2011. Foreword by Martin Davis.
Eugenio G. Omodeo
formalized logic to
Proof verification within set theory
3/26
Jacob T. Schwartz
( 1930–2009 )
Putting mathematical discourse into a form every one of whose details can be checked by a computer forces us to ‘walk in shackles’
— but then we want these shackles to be as light as possible. Eugenio G. Omodeo
Proof verification within set theory
4/26
Jacob T. Schwartz
( 1930–2009 )
Putting mathematical discourse into a form every one of whose details can be checked by a computer forces us to ‘walk in shackles’
— but then we want these shackles to be as light as possible. Eugenio G. Omodeo
Proof verification within set theory
4/26
ÆtnaNova aka Ref eree:
( On-line worksheet ) Eugenio G. Omodeo
Proof verification within set theory
5/26
Automated proof-assistants for set theory:
To cite just a few among many Ref’s competitors: Mizar: Andrzej Trybulec’s system for formal verification of proofs, with its mathematical library MML based on the Tarski-Grothendieck set theory Scunak: Chad E. Brown’s system combining type theory and untyped set theory GOEDEL: Johan G.F. Belinfante’s modification of Gödel’s algorithm for class formation, with 30 000 rewrite rules to simplify statements and expressions for
Eugenio G. Omodeo
Proof verification within set theory
6/26
Automated proof-assistants for set theory:
To cite just a few among many Ref’s competitors: Mizar: Andrzej Trybulec’s system for formal verification of proofs, with its mathematical library MML based on the Tarski-Grothendieck set theory Scunak: Chad E. Brown’s system combining type theory and untyped set theory GOEDEL: Johan G.F. Belinfante’s modification of Gödel’s algorithm for class formation, with 30 000 rewrite rules to simplify statements and expressions for
Eugenio G. Omodeo
Proof verification within set theory
6/26
Automated proof-assistants for set theory:
To cite just a few among many Ref’s competitors: Mizar: Andrzej Trybulec’s system for formal verification of proofs, with its mathematical library MML based on the Tarski-Grothendieck set theory Scunak: Chad E. Brown’s system combining type theory and untyped set theory GOEDEL: Johan G.F. Belinfante’s modification of Gödel’s algorithm for class formation, with 30 000 rewrite rules to simplify statements and expressions for classes
Eugenio G. Omodeo
Proof verification within set theory
6/26
ÆtnaNova aka Referee is:
a proof checker
Eugenio G. Omodeo
Proof verification within set theory
7/26
ÆtnaNova aka Referee is:
a proof checker not a proof discoverer
Eugenio G. Omodeo
Proof verification within set theory
7/26
ÆtnaNova aka Referee is:
rooted in set theory
Eugenio G. Omodeo
Proof verification within set theory
7/26
ÆtnaNova aka Referee is:
rooted in set theory not based on a calculus
Eugenio G. Omodeo
Proof verification within set theory
7/26
ÆtnaNova aka Referee is:
rooted in set theory no hindrance with types
Eugenio G. Omodeo
Proof verification within set theory
7/26
ÆtnaNova aka Referee is:
fed with scenarios
Eugenio G. Omodeo
Proof verification within set theory
7/26
ÆtnaNova aka Referee is:
fed with scenarios not highly interactive
Eugenio G. Omodeo
Proof verification within set theory
7/26
ÆtnaNova aka Referee is:
endowed with coarse-grained inference rules
Eugenio G. Omodeo
Proof verification within set theory
7/26
ÆtnaNova aka Referee is:
endowed with coarse-grained inference rules not based on resolution
Eugenio G. Omodeo
Proof verification within set theory
7/26
ÆtnaNova aka Referee is:
statement oriented
Eugenio G. Omodeo
Proof verification within set theory
7/26
ÆtnaNova aka Referee is:
statement oriented hints , though present, are accessory
Eugenio G. Omodeo
Proof verification within set theory
7/26
Context: Broad-gauge proof verification
Eugenio G. Omodeo
Proof verification within set theory
8/26
Context: Broad-gauge proof verification
Scenarios: Our software system ingests proofs formalized within Zermelo-Fraenkel set theory and checks their compliance with mathematical rigor
Eugenio G. Omodeo
Proof verification within set theory
8/26
Context: Broad-gauge proof verification
Scenarios: Our software system ingests proofs formalized within Zermelo-Fraenkel set theory and checks their compliance with mathematical rigor It accepts trivial steps as obvious: we aim at proofs of length comparable with common semi-formal mathematical discourse
Eugenio G. Omodeo
Proof verification within set theory
8/26
Context: Broad-gauge proof verification
Scenarios: Our software system ingests proofs formalized within Zermelo-Fraenkel set theory and checks their compliance with mathematical rigor It is able to process large proof scripts ( say dozens of thousands of proofware lines written on persistent files )
Eugenio G. Omodeo
Proof verification within set theory
8/26
A large-scale proof Our privileged “scenario” script file, which evolves in parallel with our prototype proof-checker and acts as its test suite, leads from “first principles”, namely the rudiments of set theory, to the celebrated Cauchy Integral Theorem on analytic functions of complex analysis
h
Is_analyticCF (F) → ∃ε ∈ R | ε >R 0R & h∀crv1 , crv2 | Is_CD_curv(crv1 , 0R , 1R ) & Is_CD_curv(crv2 , 0R , 1R ) & crv1 0R = crv1 1R & crv2 0R = crv2 1R & h∀x ∈ Interval(0R , 1R ) | ε >R |crv1 x −C crv2 x|C i → H 1R H1R (F, crv ) = 1 0 0 (F, crv2 )i . R
Eugenio G. Omodeo
R
Proof verification within set theory
i
9/26
Why set theory as underlying formalism
In formalizing chapters of analysis, it is convenient to follow the royal road paved by the work of Cauchy, Dedekind, Frege, Cantor, Peano, Whitehead-Russell, Zermelo-Fraenkel-von Neumann, etc.
E. Landau.
Foundations of Analysis. The arithmetic of whole, rational, irrational and complex numbers. Chelsea Publishing Co., New York, 3rd edition, 1966.
Eugenio G. Omodeo
Proof verification within set theory
10/26
Why set theory as underlying formalism
In formalizing chapters of analysis, it is convenient to follow the royal road paved by the work of Cauchy, Dedekind, Frege, Cantor, Peano, Whitehead-Russell, Zermelo-Fraenkel-von Neumann, etc. The armory of elementary inference rules can today comprehend decision algorithms, named syllogistics, for fragments of set theory
A. Ferro, E.G. Omodeo, and J.T. Schwartz. Decision procedures for elementary sublanguages of set theory. I. Multi-level syllogistic and some extensions. Comm. Pure Applied Math., 33(5):599–608, 1980.
Eugenio G. Omodeo
Proof verification within set theory
10/26
Why set theory as underlying formalism
In formalizing chapters of analysis, it is convenient to follow the royal road paved by the work of Cauchy, Dedekind, Frege, Cantor, Peano, Whitehead-Russell, Zermelo-Fraenkel-von Neumann, etc. The armory of elementary inference rules can today comprehend decision algorithms, named syllogistics, for fragments of set theory To a significant extent, the language of set theory can be exploited to specify algorithms ( executably )
Eugenio G. Omodeo
Proof verification within set theory
10/26
Why set theory as underlying formalism In formalizing chapters of analysis, it is convenient to follow the royal road paved by the work of Cauchy, Dedekind, Frege, Cantor, Peano, Whitehead-Russell, Zermelo-Fraenkel-von Neumann, etc. The armory of elementary inference rules can today comprehend decision algorithms, named syllogistics, for fragments of set theory To a significant extent, the language of set theory can be exploited to specify algorithms ( executably ) E. G. Omodeo and A. I. Tomescu. Using ÆtnaNova to formally prove that the Davis-Putnam satisfiability test is correct. Le Matematiche, 63:85–105, 2008. A preliminary version was presented at CILC’07 (Messina). Eugenio G. Omodeo
Proof verification within set theory
10/26
Set theory: Ingredients –I
Boolean operations
( save absolute complementation ): ∅, ∩, ∪, \, 4
Eugenio G. Omodeo
Proof verification within set theory
11/26
Set theory: Ingredients –I
Boolean operations
extensional ∈
( save absolute complementation ): ∅, ∩, ∪, \, 4
( two sets cannot have the same el’ts ): X = Y ↔ h∀v | v ∈ X ↔ v ∈ Y i
Eugenio G. Omodeo
Proof verification within set theory
11/26
Set theory: Ingredients –I
Boolean operations
extensional ∈
Nesting
( save absolute complementation ): ∅, ∩, ∪, \, 4
( two sets cannot have the same el’ts ): X = Y ↔ h∀v | v ∈ X ↔ v ∈ Y i
( which makes even individuals superfluous ): X with Y , { X1 , . . . , Xn }
Eugenio G. Omodeo
Proof verification within set theory
11/26
Set theory: Ingredients –I Boolean operations
extensional ∈
Nesting
( save absolute complementation ): ∅, ∩, ∪, \, 4
( two sets cannot have the same el’ts ): X = Y ↔ h∀v | v ∈ X ↔ v ∈ Y i
( which makes even individuals superfluous ): X with Y , { X1 , . . . , Xn }
Possibility to S form sets Y P(Y ) ownP(Y ) S(Y )
complying with intensional specifications : =Def { z : x ∈ Y , z ∈ x} =Def { x : x ⊆ Y } =Def { x : x ⊆ Y | x ∈ Y } {x} : x ∈ Y | x = 6 ∅ =Def
Eugenio G. Omodeo
Proof verification within set theory
11/26
Set theory: Ingredients –II
Well-foundedness and choice : arb (X ) ∈ ( X with X )
Eugenio G. Omodeo
&
X ∩ arb (X ) = ∅
Proof verification within set theory
12/26
Set theory: Ingredients –II
Well-foundedness and choice : arb (X ) ∈ ( X with X )
&
X ∩ arb (X ) = ∅
Recursion based on ∈ : ult_mm(S) =Def S ∪
Eugenio G. Omodeo
S
ult_mm(x) : x ∈ S
Proof verification within set theory
12/26
Set theory: Ingredients –II Well-foundedness and choice : arb (X ) ∈ ( X with X )
&
X ∩ arb (X ) = ∅
Recursion based on ∈ : ult_mm(S) =Def S ∪
S
ult_mm(x) : x ∈ S
Existence of infinite sets : s∞ 6= ∅
&
( Postulate! )
h∀ x ∈ s∞ | {x} ∈ s∞ i
Eugenio G. Omodeo
Proof verification within set theory
12/26
Interaction with our proof-verifier
( Input )
Tiny proof-scenario
( The actual file submitted to Ref is in keyboard-oriented format ) Eugenio G. Omodeo
Proof verification within set theory
13/26
Interaction with our proof-verifier( Output )
Eugenio G. Omodeo
Proof verification within set theory
14/26
Interaction with our proof-verifier( Output )
Eugenio G. Omodeo
Proof verification within set theory
14/26
3 basic constituents of a scenario ( examples ) Definition: -- A ‘tog’ is a self-inverse, single-valued map which is anti-diagonal. Def 119.
Is_tog(T)
↔Def Svm(T) & T← = T & {p ∈ T | p[1] = p[2] } = ∅
Theorem and Proof: -- Every infinite set supports a toggling map. Thm 998. ¬Finite(S) → h∃t | Is_tog(t) & dom(t) = Si. Proof: Suppose_not(s0 ) =⇒
.. .
.. .
T somehow =⇒
¬h∃t | Is_tog(t) & dom(t) = s0 i & ¬Finite(s0 ) .. .. . . false;
Eugenio G. Omodeo
Discharge =⇒
Qed
Proof verification within set theory
15/26
∈-recursive definitions
Besides permitting shorthands, definitions serve other purposes,
as illustrated by the rank-related definitions below:
Eugenio G. Omodeo
Proof verification within set theory
16/26
∈-recursive definitions
Besides permitting shorthands, definitions serve other purposes,
as illustrated by the rank-related definitions below: k Successor ( defined for any set, including ordinals and integers ) Def 11.
next(X) =Def X ∪ {X}
Eugenio G. Omodeo
Proof verification within set theory
16/26
∈-recursive definitions
Besides permitting shorthands, definitions serve other purposes,
as illustrated by the rank-related definitions below: k Successor ( defined for any set, including ordinals and integers ) Def 11.
next(X) =Def X ∪ {X}
k Rank of a set Def 10090.
rk(X) =Def
Eugenio G. Omodeo
S
{ next rk(y) : y ∈ X }
Proof verification within set theory
16/26
∈-recursive definitions
Besides permitting shorthands, definitions serve other purposes,
as illustrated by the rank-related definitions below: k Successor ( defined for any set, including ordinals and integers ) Def 11.
next(X) =Def X ∪ {X}
k Rank of a set Def 10090.
rk(X) =Def
S
{ next rk(y) : y ∈ X }
k X th level of the cumulative structure based on A S Def 10091. VXA =Def A ∪ { P(VyA ) : y ∈ X } Eugenio G. Omodeo
Proof verification within set theory
16/26
Definitions serve various purposes. At their simplest they are merely abbreviations which concentrate attention on interesting constructs by assigning them names which shorten their syntactic form. (But of course the compounding of such abbreviations can change the appearance of a discourse completely [· · · ] )
[· · · ] Beyond this, definitions serve to ‘instantiate’, that is, to introduce the objects whose special properties are crucial to an intended argument. Like the selection of crucial lines, points, and circles from the infinity of geometric elements that might be considered in a Euclidean argument, definitions of this kind often carry a proof’s most vital ideas. Eugenio G. Omodeo
Proof verification within set theory
17/26
Comput’nal logic V proofware engineering Container finite_induction (s0 , P(X)) Finite(s0 ) & P(s) =⇒ (fΘ ) fΘ ⊆ s0 & P(fΘ ) & h ∀ t ( fΘ | ¬ P(t) i End finite_induction
We often need to associate
some highly compound meaning
with a symbol. Such a symbol
serves us as a kind of container
carrying this meaning, always
with the understanding that it
can be opened if we need its
content. Eugenio G. Omodeo
(Gottlob Frege, 1848–1925)
Proof verification within set theory
18/26
4th , major constituent of a scenario (example) A construct for proof reuse Theory globalizeMap (t0 ) Svm(t0 ) & range(t0 ) ⊇ dom(t0 ) End globalizeMap Enter_theory globalizeMap .. .. .. .. . . . . Enter_theory Set_theory Within a scenario, the discourse can momentarily digress into a ‘Theory’ that enforces certain local assumptions. At the end of the digression, the upper theory will be re-entered. Eugenio G. Omodeo
Proof verification within set theory
19/26
4th , major constituent of a scenario (example) A construct for proof reuse Theory globalizeMap (t0 ) Svm(t0 ) & range(t0 ) ⊇ dom(t0 ) End globalizeMap Enter_theory globalizeMap .. .. .. .. . . . . Enter_theory Set_theory Within a scenario, the discourse can momentarily digress into a ‘Theory’ that enforces certain local assumptions. At the end of the digression, the upper theory will be re-entered. Eugenio G. Omodeo
Proof verification within set theory
19/26
4th , major constituent of a scenario (example)
A construct for proof reuse Theory globalizeMap (t0 ) Svm(t0 ) & range(t0 ) ⊇ dom(t0 ) =⇒ togΘ Finite(t0 ) → range(t0 ) = dom(t0 ) & 1–1(t0 ) h∀x | x ∈ / range(t0 ) → togΘ (x)6=x & togΘ togΘ (x) = xi h∀x ∈ dom(t0 ) | togΘ (x) = t0 xi End globalizeMap As an outcome of the digression, the Theory will be able to instantiate new theorems: possibly involving new symbols, whose definition it encapsulates.
Eugenio G. Omodeo
Proof verification within set theory
19/26
4th , major constituent of a scenario (example) A construct for proof reuse Theory globalizeMap (t0 ) Svm(t0 ) & range(t0 ) ⊇ dom(t0 ) =⇒ togΘ Finite(t0 ) → range(t0 ) = dom(t0 ) & 1–1(t0 ) h∀x | x ∈ / range(t0 ) → togΘ (x)6=x & togΘ togΘ (x) = xi h∀x ∈ dom(t0 ) | togΘ (x) = t0 xi End globalizeMap APPLY htogΘ : flip i globalizeMap(t0 7→ ∅) =⇒ Thm 1000. h∀x | flip(x)6=x & flip flip(x) = x i. ( A 2nd -order Skolemization ) Eugenio G. Omodeo
Proof verification within set theory
19/26
4th , major constituent of a scenario (example) A construct for proof reuse Theory globalizeMap (t0 ) Svm(t0 ) & range(t0 ) ⊇ dom(t0 ) =⇒ togΘ Finite(t0 ) → range(t0 ) = dom(t0 ) & 1–1(t0 ) h∀x | x ∈ / range(t0 ) → togΘ (x)6=x & togΘ togΘ (x) = xi h∀x ∈ dom(t0 ) | togΘ (x) = t0 xi End globalizeMap
R. Burstall and J. Goguen. Putting theories together to make specifications. In R. Reddy, ed, Proc. 5th International Joint Conference on Artificial Intelligence. Cambridge, MA, pp. 1045–1058, 1977.
Eugenio G. Omodeo
Proof verification within set theory
19/26
Proofs in Ref
( Examples )
S S Thm 2e: [Union of adjunction] (X ∪ {Y}) = Y ∪ X. Proof: S S Suppose_not(x0 , y0 ) =⇒ Stat0 : (x0 ∪ {y0 })6=y0 ∪ x0 S S hai,→Stat0 =⇒ a ∈ (x0 ∪ {y0 }) 6↔ a ∈ y0 ∪ x0
Arguing by contradiction, let x0 , y0 be a counterexample, so that in S S
either one of (x0 ∪ {y0 }) and y0 ∪ x0 there is an a not belonging
S
to the other set. Taking the definition of into account, by mono
tonicity we must exclude the possibility that a ∈ Sx0 \S(x0 ∪ {y0 });
through variable-substitution, we must also discard the possibility that
a ∈ S(x ∪ {y })\Sx \y . 0 0 0 0 Set_monot =⇒ {u : v ∈ x0 , u ∈ v} ⊆ {u : v ∈ x0 ∪ {y0 }, u ∈ v} Suppose =⇒ Stat1 :a ∈ {u : v ∈ x0 ∪ {y0 }, u ∈ v} & a ∈ / {u : v ∈ x0 , u ∈ v} & a∈ / y0 hv0 , u0 , v0S , u0 i,→Stat1 =⇒ false; Discharge =⇒ Auto Use_def( ) =⇒ Stat2 : a ∈ / {u : v ∈ x0 ∪ {y0 }, u ∈ v} & a ∈ y0
The other possibility left, that a ∈ y0 \S(x0 ∪ {y0 }), is also manifestly
absurd. This contradiction leads us to the desired conclusion. hy0 , ai,→Stat2 =⇒ false; Discharge =⇒ Qed Eugenio G. Omodeo
Proof verification within set theory
20/26
Proofs in Ref
( Examples )
Thm 31h: [Less-one lemma for union-set] S M = T\{C} & S = T ∪ X ∪ {V} & Y ∈ S ∩ {C, V} → S h∃d | (M ∪ {X ∪ {Y}}) = S\{d}i. Proof: S Suppose_not(m, t, c, s, x, v, y) =⇒ Stat0 : ¬h∃d | (m ∪ {x ∪ {y}}) = s\{d}i S & m = t\{c} & s = t ∪ xS∪ {v} & (y = v ∨ (c = y & y ∈ s))
For, supposing the contrary, (m ∪ {x ∪ {y}}) would differ from each
of s\{s}, s\{c}, and s\{v}, the first of which equals s. Thanks to
Thm 2e, we can rewrite S(m ∪ {x ∪ {y}}) as x ∪ {y} ∪ Sm; but then
the decision algorithm for a fragment of set theory known as ‘multi
level syllogistic with singleton’ yields an immediate contradiction. S hsi,→Stat0 =⇒ S(m ∪ {x ∪ {y}})6=s hci,→Stat0 =⇒ S(m ∪ {x ∪ {y}})6=s\{c} hvi,→Stat0 =⇒ (m ∪ {x ∪ {y}})6=s\{v} hm, x ∪ {y}i,→T 2e =⇒ Auto S EQUAL =⇒ Stat1 : x ∪ {y} ∪ m6=s\{c} & S S x ∪ {y} ∪ m6=s\{v} & x ∪ {y} ∪ m6=s (Stat0, Stat1)Discharge =⇒ Qed Eugenio G. Omodeo
Proof verification within set theory
20/26
Proofs in Ref
( Examples )
S Thm 32: [Finite, non-null sets own sources] Finite(F) & F6=∅ → F\ F6=∅. Proof Suppose_not(f Auto 1 ) =⇒
Arguing by contradiction, suppose that there are counterexamples to
the claim. Then, by exploiting finite induction, we can pick a minimal
counterexample, f . 0 S APPLY hfinΘ : f0 i finiteInduction s0 7→ f1 , P(S) 7→ (S6=∅ & S\ S = ∅) = S Stat0 : h∀s | s ⊆ f0 → Finite(s) & (s6=∅ & s\ s = ∅ ↔ s = f0 )i Loc_def =⇒ a = arb (f0 ) S hf0 i,→Stat0 =⇒ Stat1 : Finite(f0 ) & a ∈ f0 & f0 \ Sf0 = ∅
Momentarily supposing that f0 = {a}, one gets f0 6⊆ a, because
S S
f0 ⊆ a would imply f0 \ f0 ⊇ {a}\a and hence would imply the
emptiness of {a}\a, whence the manifest absurdity a ∈ a follows.
But, on the other hand, S{a} ⊆ a trivially holds; therefore we must
exclude that f is a singleton {a}. 0
Eugenio G. Omodeo
Proof verification within set theory
20/26
Proofs in Ref
( Examples )
S Suppose =⇒ f0 = {a} & f0 6⊆ a S EQUAL =⇒ {a} 6⊆ a S Use_def( ) =⇒ {u : v ∈ {a}, u ∈ v} 6⊆ a SIMPLF =⇒ false; Discharge =⇒ Auto
Due to our minimality assumption, the strict non-null subset
f0 \{arb (f0 )} of f0 cannot be a counterexample to the claim; therefore
it has sources and hence f0 \S(f0 \{arb (f0 )})6=∅. S S hf0 \{a}, ai,→T 2e(?) =⇒ (f0 \{a} ∪ {a}) = (f0 \{a}) ∪ a & f0 \{a} ∪ {a} = f0 S h f0 \{a}i,→Stat0(?) =⇒ f0 \ (f0 \{a})6=∅
Since arb (f0 ) does not intersect f0 , the inequality just found con
flicts with the equality f0 \ S(f0 \{arb (f0 )}) ∪ arb (f0 ) = ∅ which
one gets from Thm 2e through equality propagation. S EQUAL =⇒ f0 \ (f0 \{a}) ∪ a = ∅ Discharge =⇒ Qed
Eugenio G. Omodeo
Proof verification within set theory
20/26
Inference methods – I
1
The context of an inference step
2
The ELEM primitive
3
The Suppose primitive
4
The Discharge primitive
5
The Suppose_not and QED primitives
6
The Def and Use_def primitives “Algebraic” and recursive definitions
7
The Loc_def primitive
Eugenio G. Omodeo
Proof verification within set theory
21/26
Inference methods – II
8
The citation primitives and their instantiation mechanisms Logical equivalences exploited in instantiating statements Correspondence between substituends and substitutes used in instantiation
9
The EQUAL and ALGEBRA primitives
10
The Declare directive
11
The SIMPLF primitive
12
The Set_monot and Pred_monot primitives
Eugenio G. Omodeo
Proof verification within set theory
21/26
?
ELEM = Multilevel syllogistic
MLSS is the fragment of set theory consisting of set variables u , v , w , x , y , z , . . . operators − ∩ −, − \ −, − ∪ −, {−, . . . , −} relators − ∈ −, − = −, − ⊆ − propositional connectives ¬ − , − → − , etc.
Eugenio G. Omodeo
Proof verification within set theory
22/26
?
ELEM = Multilevel syllogistic
MLSS is the fragment of set theory consisting of set variables u , v , w , x , y , z , . . . operators − ∩ −, − \ −, − ∪ −, {−, . . . , −} relators − ∈ −, − = −, − ⊆ − propositional connectives ¬ − , − → − , etc. It turns out that either ZF ` ϕ∃ holds, for all ϕ in MLSS.
Eugenio G. Omodeo
or ZF ` ¬ ϕ∃
Proof verification within set theory
22/26
?
ELEM = Multilevel syllogistic MLSS is the fragment of set theory consisting of set variables u , v , w , x , y , z , . . . operators − ∩ −, − \ −, − ∪ −, {−, . . . , −} relators − ∈ −, − = −, − ⊆ − propositional connectives ¬ − , − → − , etc. It turns out that either ZF ` ϕ∃ holds, for all ϕ in MLSS.
or ZF ` ¬ ϕ∃
Deciding which one of the two holds is an NP-complete problem.
Eugenio G. Omodeo
Proof verification within set theory
22/26
?
ELEM = Multilevel syllogistic MLSS is the fragment of set theory consisting of set variables u , v , w , x , y , z , . . . operators − ∩ −, − \ −, − ∪ −, {−, . . . , −} relators − ∈ −, − = −, − ⊆ − propositional connectives ¬ − , − → − , etc. It turns out that either ZF ` ϕ∃ holds, for all ϕ in MLSS.
or ZF ` ¬ ϕ∃
Deciding which one of the two holds is an NP-complete problem. Our proof-checker invokes the MLSS-decider when ELEM is supplied as the justification of a step in a proof Eugenio G. Omodeo
Proof verification within set theory
22/26
A permanent decidable extension of MLSS The language of MLSS can be variously enriched with uninterpreted function symbols subject to universally quantified assumptions Example: Selector arb, pairing operator [−, −](= cons) and projections car and cdr:
h∀x | arb (x) ∈ x ∪ {x} & arb (x) ∩ x = ∅i h∀ x, y | car([x, y ]) = x i & h∀ x, y | cdr([x, y ]) = y i
which abstract w.r.t. any particular notion of pair, such as, for instance:
[x, y ] =Def x , {y }, y , x car(p) =Def arb arb(p) cdr(p) =Def car arb p \ { arb (p) } \ { arb (p) } Eugenio G. Omodeo
Proof verification within set theory
23/26
The ELEM inference mechanism
ELEM is the most central of all Ref’s inference mechanisms. Its use is, often, tacitly combined with other forms of inference.
Eugenio G. Omodeo
Proof verification within set theory
24/26
The ELEM inference mechanism ELEM implements an enhanced variant of multi-level syllogistic, a decision algorithm which determines whether a given unquantified set-theoretic formula involving only individual variables (which designate sets) and a restricted collection of set operators is satisfiable. By means of that algorithm, the Ref verifier can identify many cases in which a conjunction constructed by negating a statement S of a proof and conjoining a selection of earlier statements is unsatisfiable, so that S follows from the preceding context. Should some of the constructs appearing in this context be unamenable to Ref’s built-in syllogistic, a pre-processing phase replaces all parts of the context whose lead operators cannot be treated by the decision algorithm by new variables replacing recognizably equal parts by the same variable. Eugenio G. Omodeo
Proof verification within set theory
24/26
The ELEM inference mechanism ELEM implements an enhanced variant of multi-level syllogistic, a decision algorithm which determines whether a given unquantified set-theoretic formula involving only individual variables (which designate sets) and a restricted collection of set operators is satisfiable. By means of that algorithm, the Ref verifier can identify many cases in which a conjunction constructed by negating a statement S of a proof and conjoining a selection of earlier statements is unsatisfiable, so that S follows from the preceding context. Should some of the constructs appearing in this context be unamenable to Ref’s built-in syllogistic, a pre-processing phase replaces all parts of the context whose lead operators cannot be treated by the decision algorithm by new variables replacing recognizably equal parts by the same variable. Eugenio G. Omodeo
Proof verification within set theory
24/26
Inference methods – advanced
13
The THEORY modularization construct The ENTER_THEORY directive, the Assump primitive
14
The APPLY primitive Skolemization
15
‘AUTO’ formulae: Statements with implicit conclusions
16
The behind-the-scenes use of ELEM (“penumbra” effect)
17
The behind-the-scenes activity of proof-by-structure
18
Use of external provers
Eugenio G. Omodeo
Proof verification within set theory
25/26
Thank you for your attention!
Eugenio G. Omodeo
Proof verification within set theory
26/26