Proof verification within set theory

0 downloads 127 Views 2MB Size Report
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