This theory formalizes minimal first-order logic [Benl et al., 1998], mFOL, in Nuprl
and defines provability and uniform evidence for for formulas of mFOL.
Our soundness/completness theorem for mFOL [Constable & Bickford, 2014] states that a formula of mFOL
is provable if and only if the type of uniform evidence for it is inhabited.
We are working on a formal Nuprl proof of this completeness theorem
but that will require some new primitive operations in the Nuprl computation system.
However, we can already prove the soundness direction of the theorem
as stated here: mFOL-proveable-formula-evidence.
Some explanation of the formal statement:
Formulas of mFOL are represented by members of the type ⌈mFOL()⌉.
That type and many operators on it are automatically generated from
CreateDataType
[ `atomic`: [ name, Atom
; vars, ℤ List
]
; `connect`: [ knd, Atom
; left, mFOL()
; right, mFOL()
]
; `quant`: [ isall, 𝔹
; var, ℤ
; body, mFOL()
]
]
In the atomic case, we are using integers, ℤ, to represent variables
and Atom (essentially tokens) for names of atomic relations.
Our language thus contains only relation symbols, and contains
countably many symbols of each arity.
Since in minimal logic there is no constant for False and no unary negation
connective, all the connectives are binary and we label those with a token
(a member of type Atom). In the proof system we define for mFOL(), only the tokens
"and", "or", and "imp" are relevant as connectives.
A quantified formula is a forall or exists formula depending on the boolean, isall.
Inductive definitions over mFOL() are made using the automatically generated
induction operator that is displayed as
⌈mFOL_ind(fmla;
mFOatomic(R,vars)⇒ [atomic];
mFOconnect(connective,a,b)⇒ reca,recb.[connect];
mFOquant(isall,x,body)⇒ rec.[quant]) ⌉
In order to define provability we must define the proof rules and
to do that we must define (among other things) equality of mFOL() formulas,
mFO-equal,
the free variables of a formula,
mFOL-freevars ,
and the bound variables of a formula,
mFOL-boundvars.
Since there are no function symbols in our language, we only need to
define substitution of one variable for another, but this still requires
renaming of bound variables (and this is why we chose to represent variables
as integers -- so that it is easy to generate fresh names).
Instead of defining alpha-equality of formulas, we define the
"abstract meaning" of a formula.
An abstract formula, AbstractFOFormula, assigns a meaning
(a member of ℙ, i.e. a type) to a domain, Dom, a structure over Dom,
and an assignment into Dom. A structure, FOStruct, over Dom,
assigns a meaning to each instance of an atomic formula.
An assignment, FOAssignment, assigns a member of Dom to each variable.
The meaning assigned by abstract formula phi to a given Dom, structure S,
and assignment a, FOSatWith, is displayed as ⌈Dom,S,a |= phi⌉ .
The abstract meaning of a mFOL() formula is defined inductively by
mFOL-abstract
Alpha-equal formulas define the same abstract formula.
So, to do renaming of bound variables
we prove a lemma mFOL-bound-rename that shows that there is a formula
with the same abstract meaning whose bound variables are disjoint from
a given list of variables.
Then we use the "extract" of that lemma as the renaming operator
mFOL-rename-bound-to-avoid
Now substitution, mFOL-subst,
is done by first renaming bound variables to
avoid the new variable and then renaming the old variable to the new varaible.
A sequent for mFOL, mFOL-sequent, is a list of hypothesis and a conclusion.
The abstract meaning of a sequent mFOL-sequent-abstract is a function
from the tuple of abstract meanings of the hypotheses to the abstract meaning
of the conclusion.
To define provablity for mFOL we create another data type ⌈mFOLRule()⌉ for the
rules of mFOL. It has eleven cases corresponding to the introduction and
elimination rules for "and", "or", "imp", "all", and "exists", plus the hypothesis
rule. It is not a recursive type, but the data-type package generates a case
operator for defining operations on rules, displayed as follows:
case(<rule>)
andI => <andI>
impI => <impI>
allI with <var> => <allI>
existsI with <v1> => <existsI>
orI (left?<left>) => <orI>
hyp => <hyp>
andE @<h1> => <andE>
orE @<h2> => <orE>
impE @<h3> => <impE>
allE @<h4> with <v2> => <allE>
existsE @<h5> with <v3> => <existsE>
Now we can define the effect of a given rule on a given mFOL sequent.
If the rule does not apply, then it `fails` by producing the effect ⌈inr ⋅ ⌉
otherwise it succeeds and produces ⌈inl L⌉ where L is the list of subgoal sequents.
Here is the definition:
mFOLeffect
Using this we define provability: mFOL-proveable
making use of a generic definition of provability, Error :proveable.
It says that a sequent is provable if there is a correct proof tree.
A proof tree Error :proof-tree is a well-founded tree
(for those we use Martin-Lof's, W type, Error :W)
with a sequent and a rule labeling each node.
The proof is correct for sequent s if the sequent labeling the top node is s
and for every node, the effect of the given rule on the given sequent
does not fail and the successors of the node
are correct proofs of the generated subgoal sequents.
Since proof trees are well-founded, we may prove properties of them by induction,
and we do that to prove the main soundness therorem
mFOL-proveable-evidence
It says that from a correct proof of a mFOL sequent we may construct
uniform evidence mFOL-sequent-evidence for the sequent.
Uniform evidence for an abstract formula, fmla, is the
intersection over all domains, Dom, and all structures, S, over Dom,
of evidence for ∀a:FOAssignment(Dom). Dom,S,a |= fmla.
NOTE:
Since there are no assignments into an empty domain, this means that any
evidence works when Dom is empty, so the intersection is essentially over
non-empty domains Dom. Thus, (forall x. P(x)) => (exists x. P(x)) is uniformly valid
(i.e. has uniform evidence) so (by our completeness theorem) is provable.
A careful examination of the effect of the mFOL rules will show that it is
indeed provable.
The proof of the main soundness theorem is by induction on the correct proof tree
and reduces to twelve cases (one for each of the eleven rules except orI
which generates two cases).
The case for the hypothesis rule follows from this lemma: mFOL-sequent-evidence-trivial.
The propositional cases are fairly straightforward, using these lemmas:
mFOL-sequent-evidence_transitivity1,
mFOL-sequent-evidence_transitivity2,
and mFOL-sequent-evidence_and.
The quantifier cases, for allI, allE, existsI, existsE are trickier
but follow essentially from mFOL-subst-abstract.
⋅
Definition: FOAssignment
An assignment assigns a member of Dom to each variable.
(Variables in mFOL() formulas are represented by integers).⋅
FOAssignment(Dom) == ℤ ─→ Dom
Lemma: FOAssignment_wf
∀[Dom:Type]. (FOAssignment(Dom) ∈ Type)
Definition: FOStruct
A structure over Dom,
assigns a meaning to each instance of an atomic formula.⋅
FOStruct(Dom) == Atom ─→ (Dom List) ─→ ℙ
Lemma: FOStruct_wf
∀[Dom:Type]. (FOStruct(Dom) ∈ 𝕌')
Definition: update-assignment
a[x := v] == λz.if (z =z x) then v else a z fi
Lemma: update-assignment_wf
∀[Dom:Type]. ∀[a:FOAssignment(Dom)]. ∀[x:ℤ]. ∀[v:Dom]. (a[x := v] ∈ FOAssignment(Dom))
Definition: AbstractFOFormula
AbstractFOFormula == Dom:Type ─→ S:FOStruct(Dom) ─→ FOAssignment(Dom) ─→ ℙ
Lemma: AbstractFOFormula_wf
AbstractFOFormula ∈ 𝕌'
Definition: FOSatWith
An abstract formula is a function that assigns a meaning (a proposition)
to a given Dom, structure S, and assignment a. So, this definition is mainly
for notation.⋅
Dom,S,a |= fmla == fmla Dom S a
Lemma: FOSatWith_wf
∀[Dom:Type]. ∀[S:FOStruct(Dom)]. ∀[a:FOAssignment(Dom)]. ∀[fmla:AbstractFOFormula]. (Dom,S,a |= fmla ∈ ℙ)
Definition: mFO-uniform-evidence
An abstract formula fmla is true given domain Dom and structure S over Dom
if it is true for any assignment into Dom of its free variables.
Evidence for that is given by the proposition (type)
∀a:FOAssignment(Dom). Dom,S,a |= fmla
Uniform evidence for an abstract formula, fmla, is the
intersection over all domains, Dom, and all structures, S, over Dom,
of that evidence.⋅
mFO-uniform-evidence{i:l}(fmla) == ∩Dom:Type. ∩S:FOStruct(Dom). ∀a:FOAssignment(Dom). Dom,S,a |= fmla
Lemma: mFO-uniform-evidence_wf
∀[fmla:AbstractFOFormula]. (mFO-uniform-evidence{i:l}(fmla) ∈ 𝕌')
Definition: AbstractFOAtomic
If S is a structure (for a domain Dom), then ⌈S n ∈ (Dom List) ─→ ℙ⌉.
If a is an assignment on Dom, then ⌈map(a;L) ∈ Dom List⌉. Thus, the
meaning of the atomic formula ⌈n(L)⌉
(which is predicate symbol ⌈n ∈ Atom⌉ applied to variable list ⌈L ∈ ℤ List⌉)
is S n map(a;L)⋅
AbstractFOAtomic(n;L) == λDom,S,a. (S n map(a;L))
Lemma: AbstractFOAtomic_wf
∀[n:Atom]. ∀[L:ℤ List]. (AbstractFOAtomic(n;L) ∈ AbstractFOFormula)
Definition: FOConnective
FOConnective(knd) ==
λx,y,Dom,S,a. let p = Dom,S,a |= x in
let q = Dom,S,a |= y in
if knd =a "and" then p ∧ q
if knd =a "or" then p ∨ q
else p ⇒ q
fi
Lemma: FOConnective_wf
∀knd:Atom. (FOConnective(knd) ∈ AbstractFOFormula ─→ AbstractFOFormula ─→ AbstractFOFormula)
Definition: FOQuantifier
FOQuantifier(isall) ==
λx,fmla,Dom,S,a. if isall then ∀v:Dom. Dom,S,a[x := v] |= fmla else ∃v:Dom. Dom,S,a[x := v] |= fmla fi
Lemma: FOQuantifier_wf
∀[isall:𝔹]. (FOQuantifier(isall) ∈ ℤ ─→ AbstractFOFormula ─→ AbstractFOFormula)
Definition: mFOLco
mFOLco() ==
corec(X.lbl:Atom × if lbl =a "atomic" then name:Atom × (ℤ List)
if lbl =a "connect" then knd:Atom × left:X × X
if lbl =a "quant" then isall:𝔹 × var:ℤ × X
else Void
fi )
Lemma: mFOLco_wf
mFOLco() ∈ Type
Lemma: mFOLco-ext
mFOLco() ≡ lbl:Atom × if lbl =a "atomic" then name:Atom × (ℤ List)
if lbl =a "connect" then knd:Atom × left:mFOLco() × mFOLco()
if lbl =a "quant" then isall:𝔹 × var:ℤ × mFOLco()
else Void
fi
Definition: mFOLco_size
mFOLco_size(p) ==
fix((λsize,p. let lbl,x = p
in if lbl =a "atomic" then 0
if lbl =a "connect" then let knd,left,z = x in (1 + (size left)) + (size z)
if lbl =a "quant" then let isall,var,z = x in 1 + (size z)
else 0
fi ))
p
Lemma: mFOLco_size_wf
∀[p:mFOLco()]. (mFOLco_size(p) ∈ partial(ℕ))
Definition: mFOL
mFOL() == {p:mFOLco()| (mFOLco_size(p))↓}
Lemma: mFOL_wf
mFOL() ∈ Type
Definition: mFOL_size
mFOL_size(p) ==
fix((λsize,p. let lbl,x = p
in if lbl =a "atomic" then 0
if lbl =a "connect" then let knd,left,z = x in (1 + (size left)) + (size z)
if lbl =a "quant" then let isall,var,z = x in 1 + (size z)
else 0
fi ))
p
Lemma: mFOL_size_wf
∀[p:mFOL()]. (mFOL_size(p) ∈ ℕ)
Lemma: mFOL-ext
mFOL() ≡ lbl:Atom × if lbl =a "atomic" then name:Atom × (ℤ List)
if lbl =a "connect" then knd:Atom × left:mFOL() × mFOL()
if lbl =a "quant" then isall:𝔹 × var:ℤ × mFOL()
else Void
fi
Definition: mFOatomic
name(vars) == <"atomic", name, vars>
Lemma: mFOatomic_wf
∀[name:Atom]. ∀[vars:ℤ List]. (name(vars) ∈ mFOL())
Definition: mFOconnect
mFOconnect(knd;left;right) == <"connect", knd, left, right>
Lemma: mFOconnect_wf
∀[knd:Atom]. ∀[left,right:mFOL()]. (mFOconnect(knd;left;right) ∈ mFOL())
Definition: mFOquant
mFOquant(isall;var;body) == <"quant", isall, var, body>
Lemma: mFOquant_wf
∀[isall:𝔹]. ∀[var:ℤ]. ∀[body:mFOL()]. (mFOquant(isall;var;body) ∈ mFOL())
Definition: mFOatomic?
mFOatomic?(v) == fst(v) =a "atomic"
Lemma: mFOatomic?_wf
∀[v:mFOL()]. (mFOatomic?(v) ∈ 𝔹)
Definition: mFOatomic-name
mFOatomic-name(v) == fst(snd(v))
Lemma: mFOatomic-name_wf
∀[v:mFOL()]. mFOatomic-name(v) ∈ Atom supposing ↑mFOatomic?(v)
Definition: mFOatomic-vars
mFOatomic-vars(v) == snd(snd(v))
Lemma: mFOatomic-vars_wf
∀[v:mFOL()]. mFOatomic-vars(v) ∈ ℤ List supposing ↑mFOatomic?(v)
Definition: mFOconnect?
mFOconnect?(v) == fst(v) =a "connect"
Lemma: mFOconnect?_wf
∀[v:mFOL()]. (mFOconnect?(v) ∈ 𝔹)
Definition: mFOconnect-knd
mFOconnect-knd(v) == fst(snd(v))
Lemma: mFOconnect-knd_wf
∀[v:mFOL()]. mFOconnect-knd(v) ∈ Atom supposing ↑mFOconnect?(v)
Definition: mFOconnect-left
mFOconnect-left(v) == fst(snd(snd(v)))
Lemma: mFOconnect-left_wf
∀[v:mFOL()]. mFOconnect-left(v) ∈ mFOL() supposing ↑mFOconnect?(v)
Definition: mFOconnect-right
mFOconnect-right(v) == snd(snd(snd(v)))
Lemma: mFOconnect-right_wf
∀[v:mFOL()]. mFOconnect-right(v) ∈ mFOL() supposing ↑mFOconnect?(v)
Definition: mFOquant?
mFOquant?(v) == fst(v) =a "quant"
Lemma: mFOquant?_wf
∀[v:mFOL()]. (mFOquant?(v) ∈ 𝔹)
Definition: mFOquant-isall
mFOquant-isall(v) == fst(snd(v))
Lemma: mFOquant-isall_wf
∀[v:mFOL()]. mFOquant-isall(v) ∈ 𝔹 supposing ↑mFOquant?(v)
Definition: mFOquant-var
mFOquant-var(v) == fst(snd(snd(v)))
Lemma: mFOquant-var_wf
∀[v:mFOL()]. mFOquant-var(v) ∈ ℤ supposing ↑mFOquant?(v)
Definition: mFOquant-body
mFOquant-body(v) == snd(snd(snd(v)))
Lemma: mFOquant-body_wf
∀[v:mFOL()]. mFOquant-body(v) ∈ mFOL() supposing ↑mFOquant?(v)
Lemma: mFOL-induction
∀[P:mFOL() ─→ ℙ]
((∀name:Atom. ∀vars:ℤ List. P[name(vars)])
⇒ (∀knd:Atom. ∀left,right:mFOL(). (P[left] ⇒ P[right] ⇒ P[mFOconnect(knd;left;right)]))
⇒ (∀isall:𝔹. ∀var:ℤ. ∀body:mFOL(). (P[body] ⇒ P[mFOquant(isall;var;body)]))
⇒ {∀v:mFOL(). P[v]})
Lemma: mFOL-definition
∀[A:Type]. ∀[R:A ─→ mFOL() ─→ ℙ].
((∀name:Atom. ∀vars:ℤ List. {x:A| R[x;name(vars)]} )
⇒ (∀knd:Atom. ∀left,right:mFOL(). ({x:A| R[x;left]} ⇒ {x:A| R[x;right]} ⇒ {x:A| R[x;mFOconnect(knd;left;right)]}\000C ))
⇒ (∀isall:𝔹. ∀var:ℤ. ∀body:mFOL(). ({x:A| R[x;body]} ⇒ {x:A| R[x;mFOquant(isall;var;body)]} ))
⇒ {∀v:mFOL(). {x:A| R[x;v]} })
Definition: mFOL_ind
mFOL_ind(v;
mFOatomic(name,vars)⇒ atomic[name; vars];
mFOconnect(knd,left,right)⇒ rec1,rec2.connect[knd; left; right; rec1; rec2];
mFOquant(isall,var,body)⇒ rec3.quant[isall; var; body; rec3]) ==
fix((λmFOL_ind,v. let lbl,v1 = v
in if lbl="atomic" then let name,v2 = v1 in atomic[name; v2]
if lbl="connect"
then let knd,v2 = v1
in let left,v3 = v2
in connect[knd; left; v3; mFOL_ind left; mFOL_ind v3]
if lbl="quant" then let isall,v2 = v1 in let var,v3 = v2 in quant[isall; var; v3; mFOL_ind v3]
else ⊥
fi ))
v
Lemma: mFOL_ind_wf
∀[A:Type]. ∀[R:A ─→ mFOL() ─→ ℙ]. ∀[v:mFOL()]. ∀[atomic:name:Atom ─→ vars:(ℤ List) ─→ {x:A| R[x;name(vars)]} ].
∀[connect:knd:Atom
─→ left:mFOL()
─→ right:mFOL()
─→ {x:A| R[x;left]}
─→ {x:A| R[x;right]}
─→ {x:A| R[x;mFOconnect(knd;left;right)]} ]. ∀[quant:isall:𝔹
─→ var:ℤ
─→ body:mFOL()
─→ {x:A| R[x;body]}
─→ {x:A| R[x;mFOquant(isall;var;body)]} ].
(mFOL_ind(v;
mFOatomic(name,vars)⇒ atomic[name;vars];
mFOconnect(knd,left,right)⇒ rec1,rec2.connect[knd;left;right;rec1;rec2];
mFOquant(isall,var,body)⇒ rec3.quant[isall;var;body;rec3]) ∈ {x:A| R[x;v]} )
Lemma: mFOL_ind_wf_simple
∀[A:Type]. ∀[v:mFOL()]. ∀[atomic:name:Atom ─→ vars:(ℤ List) ─→ A]. ∀[connect:knd:Atom
─→ left:mFOL()
─→ right:mFOL()
─→ A
─→ A
─→ A]. ∀[quant:isall:𝔹
─→ var:ℤ
─→ body:mFOL()
─→ A
─→ A].
(mFOL_ind(v;
mFOatomic(name,vars)⇒ atomic[name;vars];
mFOconnect(knd,left,right)⇒ rec1,rec2.connect[knd;left;right;rec1;rec2];
mFOquant(isall,var,body)⇒ rec3.quant[isall;var;body;rec3]) ∈ A)
Definition: mFOLvar
vn == n
Lemma: mFOLvar_wf
∀[n:ℤ]. (vn ∈ ℤ)
Definition: nobrackets
(nobrackets):: l == l
Definition: mFO-dest-atomic
let a,b = dest-atomic(fmla) in
F[a; b] ==
if mFOatomic?(fmla) then F[mFOatomic-name(fmla); mFOatomic-vars(fmla)] else inr ⋅ fi
Lemma: mFO-dest-atomic_wf
∀[T:Type]. ∀[F:Atom ─→ (ℤ List) ─→ (T?)]. ∀[fmla:mFOL()]. (let nm,vars = dest-atomic(fmla) inF[nm;vars] ∈ T?)
Definition: mFO-dest-connective
let a,b = dest-knd(fmla) in
F[a; b] ==
if mFOconnect?(fmla) ∧b mFOconnect-knd(fmla) =a knd
then F[mFOconnect-left(fmla); mFOconnect-right(fmla)]
else inr ⋅
fi
Lemma: mFO-dest-connective_wf
∀[T:Type]. ∀[F:mFOL() ─→ mFOL() ─→ (T?)]. ∀[fmla:mFOL()]. ∀[knd:Atom]. (let a,b = dest-knd(fmla) in F[a;b] ∈ T?)
Definition: mFO-dest-quantifier
let v,b = dest-if isall then all else exists(fmla); in
F[v; b] ==
if mFOquant?(fmla) ∧b mFOquant-isall(fmla) =b isall then F[mFOquant-var(fmla); mFOquant-body(fmla)] else inr ⋅ fi
Lemma: mFO-dest-quantifier_wf
∀[T:Type]. ∀[F:ℤ ─→ mFOL() ─→ (T?)]. ∀[fmla:mFOL()]. ∀[isall:𝔹].
(let v,b = dest-if isall then all else exists(fmla); in
F[v;b] ∈ T?)
Definition: mFO-equal
mFO-equal(x) ==
mFOL_ind(x;
mFOatomic(R,vars)⇒ λy.let R',vars' = dest-atomic(y) in
R =a R' ∧b (list-deq(IntDeq) vars vars');
mFOconnect(knd,a,b)⇒ eqa,eqb.λy.let a',b' = dest-knd(y) in
(eqa a') ∧b (eqb b');
mFOquant(isall,v,b)⇒ eqb.λy.let w,b' = dest-if isall then all else exists(y); in
(v =z w) ∧b (eqb b'))
Lemma: mFO-equal_wf
∀[x:mFOL()]. (mFO-equal(x) ∈ mFOL() ─→ 𝔹)
Definition: eq_mFO
eq_mFO(x;y) == mFO-equal(x) y
Lemma: eq_mFO_wf
∀[x,y:mFOL()]. (eq_mFO(x;y) ∈ 𝔹)
Lemma: assert-eq_mFO
∀[x,y:mFOL()]. uiff(↑eq_mFO(x;y);x = y ∈ mFOL())
Definition: deq-mFO
deq-mFO() == λx,y. eq_mFO(x;y)
Lemma: deq-mFO_wf
deq-mFO() ∈ EqDecider(mFOL())
Definition: mFOL-freevars
mFOL-freevars(fmla) ==
mFOL_ind(fmla;
mFOatomic(R,vars)⇒ remove-repeats(IntDeq;vars);
mFOconnect(knd,a,b)⇒ fvsa,fvsb.val-union(IntDeq;fvsa;fvsb);
mFOquant(isall,z,body)⇒ fvsbody.filter(λx.(¬b(x =z z));fvsbody))
Lemma: mFOL-freevars_wf
∀[fmla:mFOL()]. (mFOL-freevars(fmla) ∈ ℤ List)
Definition: mFOL-boundvars
mFOL-boundvars(fmla) ==
mFOL_ind(fmla;
mFOatomic(R,vars)⇒ [];
mFOconnect(knd,a,b)⇒ bvsa,bvsb.bvsa ∪ bvsb;
mFOquant(isall,z,body)⇒ bvsbody.insert(z;bvsbody))
Lemma: mFOL-boundvars_wf
∀[fmla:mFOL()]. (mFOL-boundvars(fmla) ∈ ℤ List)
Definition: mFOL-rename
mFOL-rename(fmla;old;new) ==
mFOL_ind(fmla;
mFOatomic(R,vars)⇒ R(map(λv.if (v =z old) then new else v fi ;vars));
mFOconnect(knd,a,b)⇒ a',b'.mFOconnect(knd;a';b');
mFOquant(isall,x,body)⇒ body'.mFOquant(isall;x;if (x =z old) then body else body' fi ))
Lemma: mFOL-rename_wf
∀[fmla:mFOL()]. ∀[old,new:ℤ]. (mFOL-rename(fmla;old;new) ∈ mFOL())
Lemma: mFOL-boundvars-of-rename
∀[fmla:mFOL()]. ∀[old,new:ℤ]. (mFOL-boundvars(mFOL-rename(fmla;old;new)) = mFOL-boundvars(fmla) ∈ (ℤ List))
Definition: mFOL-abstract
The abstract meaning of a mFOL() formula defined inductively.
Alpha-equal formulas define the same abstract formula.⋅
mFOL-abstract(fmla) ==
mFOL_ind(fmla;
mFOatomic(R,vars)⇒ AbstractFOAtomic(R;vars);
mFOconnect(knd,a,b)⇒ r1,r2.FOConnective(knd) r1 r2;
mFOquant(isall,x,body)⇒ r.FOQuantifier(isall) x r)
Lemma: mFOL-abstract_wf
∀[fmla:mFOL()]. (mFOL-abstract(fmla) ∈ AbstractFOFormula)
Lemma: mFOL-abstract-functionality
∀[fmla:mFOL()]. ∀[Dom:Type]. ∀[S:FOStruct(Dom)]. ∀[a1,a2:FOAssignment(Dom)].
Dom,S,a1 |= mFOL-abstract(fmla) = Dom,S,a2 |= mFOL-abstract(fmla) ∈ ℙ
supposing ∀z:ℤ. ((z ∈ mFOL-freevars(fmla)) ⇒ ((a1 z) = (a2 z) ∈ Dom))
Lemma: mFOL-abstract-rename
∀[Dom:Type]. ∀[S:FOStruct(Dom)].
∀x,y:ℤ. ∀fmla:mFOL().
((¬(x ∈ mFOL-boundvars(fmla)))
⇒ (∀a1,a2:FOAssignment(Dom).
((a2 = a1[y := a1 x] ∈ FOAssignment(Dom))
⇒ (Dom,S,a2 |= mFOL-abstract(fmla) = Dom,S,a1 |= mFOL-abstract(mFOL-rename(fmla;y;x)) ∈ ℙ))))
Lemma: mFOL-bound-rename
This lemma shows that there is a formula
with the same abstract meaning whose bound variables are disjoint from
a given list of variables.⋅
∀fmla:mFOL(). ∀L:ℤ List.
(∃fmla':{mFOL()| ((mFOL-abstract(fmla') = mFOL-abstract(fmla) ∈ AbstractFOFormula)
∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla')))})
Definition: mFOL-rename-bound-to-avoid
A renaming operator on mFOL() formulas.
It renames the bound variables to be disjoint from the given list
and produces a formula (alpha-equivalent) with the same abstract meaning.⋅
mFOL-rename-bound-to-avoid(fmla;L) == TERMOF{mFOL-bound-rename:o, 1:l, 1:l} fmla L
Lemma: mFOL-rename-bound-to-avoid_wf
∀fmla:mFOL(). ∀L:ℤ List.
(mFOL-rename-bound-to-avoid(fmla;L) ∈ {fmla':mFOL()|
(mFOL-abstract(fmla') = mFOL-abstract(fmla) ∈ AbstractFOFormula)
∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla'))} )
Definition: mFOL-subst
Substitute variable nw for variable old in fmla.
To do that, first rename the bound variables to avoid nw
and then rename old to nw.⋅
fmla[nw/old] == mFOL-rename(mFOL-rename-bound-to-avoid(fmla;[nw]);old;nw)
Lemma: mFOL-subst_wf
∀[fmla:mFOL()]. ∀[nw,old:ℤ]. (fmla[nw/old] ∈ mFOL())
Lemma: mFOL-subst-abstract
The evidence that fmla[x/y] in Dom, S, a is the same as the evidence
that fmla is true in Dom, S, a[y := a x].⋅
∀[Dom:Type]. ∀[S:FOStruct(Dom)]. ∀[a:FOAssignment(Dom)]. ∀[fmla:mFOL()]. ∀[x,y:ℤ].
(Dom,S,a |= mFOL-abstract(fmla[x/y]) = Dom,S,a[y := a x] |= mFOL-abstract(fmla) ∈ ℙ)
Definition: mFOL-evidence
mFOL-evidence(fmla) == mFO-uniform-evidence{i:l}(mFOL-abstract(fmla))
Lemma: mFOL-evidence_wf
∀[fmla:mFOL()]. (mFOL-evidence(fmla) ∈ 𝕌')
Lemma: mFOL-evidence-value-type
∀[fmla:mFOL()]. value-type(mFOL-evidence(fmla))
Definition: mFOLisImp
mFOLisImp(A) == mFOconnect?(A) ∧b mFOconnect-knd(A) =a "imp"
Lemma: mFOLisImp_wf
∀[A:mFOL()]. (mFOLisImp(A) ∈ 𝔹)
Definition: mFOLisAll
mFOLisAll(A) == mFOquant?(A) ∧b mFOquant-isall(A)
Lemma: mFOLisAll_wf
∀[A:mFOL()]. (mFOLisAll(A) ∈ 𝔹)
Definition: mFOLRule
mFOLRule() ==
lbl:Atom × if lbl =a "andI" then Unit
if lbl =a "impI" then Unit
if lbl =a "allI" then ℤ
if lbl =a "existsI" then ℤ
if lbl =a "orI" then 𝔹
if lbl =a "hyp" then Unit
if lbl =a "andE" then ℕ
if lbl =a "orE" then ℕ
if lbl =a "impE" then ℕ
if lbl =a "allE" then hypnum:ℕ × ℤ
if lbl =a "existsE" then hypnum:ℕ × ℤ
else Void
fi
Lemma: mFOLRule_wf
mFOLRule() ∈ Type
Lemma: mFOLRule-ext
mFOLRule() ≡ lbl:Atom × if lbl =a "andI" then Unit
if lbl =a "impI" then Unit
if lbl =a "allI" then ℤ
if lbl =a "existsI" then ℤ
if lbl =a "orI" then 𝔹
if lbl =a "hyp" then Unit
if lbl =a "andE" then ℕ
if lbl =a "orE" then ℕ
if lbl =a "impE" then ℕ
if lbl =a "allE" then hypnum:ℕ × ℤ
if lbl =a "existsE" then hypnum:ℕ × ℤ
else Void
fi
Definition: mRuleandI
andI == <"andI", ⋅>
Lemma: mRuleandI_wf
andI ∈ mFOLRule()
Definition: mRuleimpI
impI == <"impI", ⋅>
Lemma: mRuleimpI_wf
impI ∈ mFOLRule()
Definition: mRuleallI
allI with var == <"allI", var>
Lemma: mRuleallI_wf
∀[var:ℤ]. (allI with var ∈ mFOLRule())
Definition: mRuleexistsI
existsI with var == <"existsI", var>
Lemma: mRuleexistsI_wf
∀[var:ℤ]. (existsI with var ∈ mFOLRule())
Definition: mRuleorI
mRuleorI(left) == <"orI", left>
Lemma: mRuleorI_wf
∀[left:𝔹]. (mRuleorI(left) ∈ mFOLRule())
Definition: mRulehyp
hyp == <"hyp", ⋅>
Lemma: mRulehyp_wf
hyp ∈ mFOLRule()
Definition: mRuleandE
andE on hypnum == <"andE", hypnum>
Lemma: mRuleandE_wf
∀[hypnum:ℕ]. (andE on hypnum ∈ mFOLRule())
Definition: mRuleorE
orE on hypnum == <"orE", hypnum>
Lemma: mRuleorE_wf
∀[hypnum:ℕ]. (orE on hypnum ∈ mFOLRule())
Definition: mRuleimpE
impE on hypnum == <"impE", hypnum>
Lemma: mRuleimpE_wf
∀[hypnum:ℕ]. (impE on hypnum ∈ mFOLRule())
Definition: mRuleallE
allE on hypnum with var == <"allE", hypnum, var>
Lemma: mRuleallE_wf
∀[hypnum:ℕ]. ∀[var:ℤ]. (allE on hypnum with var ∈ mFOLRule())
Definition: mRuleexistsE
existsE on hypnum with var == <"existsE", hypnum, var>
Lemma: mRuleexistsE_wf
∀[hypnum:ℕ]. ∀[var:ℤ]. (existsE on hypnum with var ∈ mFOLRule())
Definition: mRuleandI?
mRuleandI?(v) == fst(v) =a "andI"
Lemma: mRuleandI?_wf
∀[v:mFOLRule()]. (mRuleandI?(v) ∈ 𝔹)
Definition: mRuleimpI?
mRuleimpI?(v) == fst(v) =a "impI"
Lemma: mRuleimpI?_wf
∀[v:mFOLRule()]. (mRuleimpI?(v) ∈ 𝔹)
Definition: mRuleallI?
mRuleallI?(v) == fst(v) =a "allI"
Lemma: mRuleallI?_wf
∀[v:mFOLRule()]. (mRuleallI?(v) ∈ 𝔹)
Definition: mRuleallI-var
mRuleallI-var(v) == snd(v)
Lemma: mRuleallI-var_wf
∀[v:mFOLRule()]. mRuleallI-var(v) ∈ ℤ supposing ↑mRuleallI?(v)
Definition: mRuleexistsI?
mRuleexistsI?(v) == fst(v) =a "existsI"
Lemma: mRuleexistsI?_wf
∀[v:mFOLRule()]. (mRuleexistsI?(v) ∈ 𝔹)
Definition: mRuleexistsI-var
mRuleexistsI-var(v) == snd(v)
Lemma: mRuleexistsI-var_wf
∀[v:mFOLRule()]. mRuleexistsI-var(v) ∈ ℤ supposing ↑mRuleexistsI?(v)
Definition: mRuleorI?
mRuleorI?(v) == fst(v) =a "orI"
Lemma: mRuleorI?_wf
∀[v:mFOLRule()]. (mRuleorI?(v) ∈ 𝔹)
Definition: mRuleorI-left
mRuleorI-left(v) == snd(v)
Lemma: mRuleorI-left_wf
∀[v:mFOLRule()]. mRuleorI-left(v) ∈ 𝔹 supposing ↑mRuleorI?(v)
Definition: mRulehyp?
mRulehyp?(v) == fst(v) =a "hyp"
Lemma: mRulehyp?_wf
∀[v:mFOLRule()]. (mRulehyp?(v) ∈ 𝔹)
Definition: mRuleandE?
mRuleandE?(v) == fst(v) =a "andE"
Lemma: mRuleandE?_wf
∀[v:mFOLRule()]. (mRuleandE?(v) ∈ 𝔹)
Definition: mRuleandE-hypnum
mRuleandE-hypnum(v) == snd(v)
Lemma: mRuleandE-hypnum_wf
∀[v:mFOLRule()]. mRuleandE-hypnum(v) ∈ ℕ supposing ↑mRuleandE?(v)
Definition: mRuleorE?
mRuleorE?(v) == fst(v) =a "orE"
Lemma: mRuleorE?_wf
∀[v:mFOLRule()]. (mRuleorE?(v) ∈ 𝔹)
Definition: mRuleorE-hypnum
mRuleorE-hypnum(v) == snd(v)
Lemma: mRuleorE-hypnum_wf
∀[v:mFOLRule()]. mRuleorE-hypnum(v) ∈ ℕ supposing ↑mRuleorE?(v)
Definition: mRuleimpE?
mRuleimpE?(v) == fst(v) =a "impE"
Lemma: mRuleimpE?_wf
∀[v:mFOLRule()]. (mRuleimpE?(v) ∈ 𝔹)
Definition: mRuleimpE-hypnum
mRuleimpE-hypnum(v) == snd(v)
Lemma: mRuleimpE-hypnum_wf
∀[v:mFOLRule()]. mRuleimpE-hypnum(v) ∈ ℕ supposing ↑mRuleimpE?(v)
Definition: mRuleallE?
mRuleallE?(v) == fst(v) =a "allE"
Lemma: mRuleallE?_wf
∀[v:mFOLRule()]. (mRuleallE?(v) ∈ 𝔹)
Definition: mRuleallE-hypnum
mRuleallE-hypnum(v) == fst(snd(v))
Lemma: mRuleallE-hypnum_wf
∀[v:mFOLRule()]. mRuleallE-hypnum(v) ∈ ℕ supposing ↑mRuleallE?(v)
Definition: mRuleallE-var
mRuleallE-var(v) == snd(snd(v))
Lemma: mRuleallE-var_wf
∀[v:mFOLRule()]. mRuleallE-var(v) ∈ ℤ supposing ↑mRuleallE?(v)
Definition: mRuleexistsE?
mRuleexistsE?(v) == fst(v) =a "existsE"
Lemma: mRuleexistsE?_wf
∀[v:mFOLRule()]. (mRuleexistsE?(v) ∈ 𝔹)
Definition: mRuleexistsE-hypnum
mRuleexistsE-hypnum(v) == fst(snd(v))
Lemma: mRuleexistsE-hypnum_wf
∀[v:mFOLRule()]. mRuleexistsE-hypnum(v) ∈ ℕ supposing ↑mRuleexistsE?(v)
Definition: mRuleexistsE-var
mRuleexistsE-var(v) == snd(snd(v))
Lemma: mRuleexistsE-var_wf
∀[v:mFOLRule()]. mRuleexistsE-var(v) ∈ ℤ supposing ↑mRuleexistsE?(v)
Lemma: mFOLRule-induction
∀[P:mFOLRule() ─→ ℙ]
(P[andI]
⇒ P[impI]
⇒ (∀var:ℤ. P[allI with var])
⇒ (∀var:ℤ. P[existsI with var])
⇒ (∀left:𝔹. P[mRuleorI(left)])
⇒ P[hyp]
⇒ (∀hypnum:ℕ. P[andE on hypnum])
⇒ (∀hypnum:ℕ. P[orE on hypnum])
⇒ (∀hypnum:ℕ. P[impE on hypnum])
⇒ (∀hypnum:ℕ. ∀var:ℤ. P[allE on hypnum with var])
⇒ (∀hypnum:ℕ. ∀var:ℤ. P[existsE on hypnum with var])
⇒ {∀v:mFOLRule(). P[v]})
Lemma: mFOLRule-definition
∀[A:Type]. ∀[R:A ─→ mFOLRule() ─→ ℙ].
({x:A| R[x;andI]}
⇒ {x:A| R[x;impI]}
⇒ (∀var:ℤ. {x:A| R[x;allI with var]} )
⇒ (∀var:ℤ. {x:A| R[x;existsI with var]} )
⇒ (∀left:𝔹. {x:A| R[x;mRuleorI(left)]} )
⇒ {x:A| R[x;hyp]}
⇒ (∀hypnum:ℕ. {x:A| R[x;andE on hypnum]} )
⇒ (∀hypnum:ℕ. {x:A| R[x;orE on hypnum]} )
⇒ (∀hypnum:ℕ. {x:A| R[x;impE on hypnum]} )
⇒ (∀hypnum:ℕ. ∀var:ℤ. {x:A| R[x;allE on hypnum with var]} )
⇒ (∀hypnum:ℕ. ∀var:ℤ. {x:A| R[x;existsE on hypnum with var]} )
⇒ {∀v:mFOLRule(). {x:A| R[x;v]} })
Definition: mFOLRule_ind
mFOLRule_ind(v;
andI;
impI;
var.allI[var];
var.existsI[var];
left.orI[left];
hyp;hypnum.andE[hypnum];
hypnum.orE[hypnum];
hypnum.impE[hypnum];
hypnum,var.allE[hypnum; var];
hypnum,var.existsE[hypnum; var]) ==
let lbl,v1 = v
in if lbl="andI" then andI
if lbl="impI" then impI
if lbl="allI" then allI[v1]
if lbl="existsI" then existsI[v1]
if lbl="orI" then orI[v1]
if lbl="hyp" then hyp
if lbl="andE" then andE[v1]
if lbl="orE" then orE[v1]
if lbl="impE" then impE[v1]
if lbl="allE" then let hypnum,v2 = v1 in allE[hypnum; v2]
if lbl="existsE" then let hypnum,v2 = v1 in existsE[hypnum; v2]
else ⊥
fi
Lemma: mFOLRule_ind_wf
∀[A:Type]. ∀[R:A ─→ mFOLRule() ─→ ℙ]. ∀[v:mFOLRule()]. ∀[andI:{x:A| R[x;andI]} ]. ∀[impI:{x:A| R[x;impI]} ].
∀[allI:var:ℤ ─→ {x:A| R[x;allI with var]} ]. ∀[existsI:var:ℤ ─→ {x:A| R[x;existsI with var]} ].
∀[orI:left:𝔹 ─→ {x:A| R[x;mRuleorI(left)]} ]. ∀[hyp:{x:A| R[x;hyp]} ]. ∀[andE:hypnum:ℕ ─→ {x:A| R[x;andE on hypnum]} ].
∀[orE:hypnum:ℕ ─→ {x:A| R[x;orE on hypnum]} ]. ∀[impE:hypnum:ℕ ─→ {x:A| R[x;impE on hypnum]} ].
∀[allE:hypnum:ℕ ─→ var:ℤ ─→ {x:A| R[x;allE on hypnum with var]} ]. ∀[existsE:hypnum:ℕ
─→ var:ℤ
─→ {x:A| R[x;existsE on hypnum with var]} ].
(mFOLRule_ind(v;
andI;
impI;
var.allI[var];
var.existsI[var];
left.orI[left];
hyp;hypnum.andE[hypnum];
hypnum.orE[hypnum];
hypnum.impE[hypnum];
hypnum,var.allE[hypnum;var];
hypnum,var.existsE[hypnum;var]) ∈ {x:A| R[x;v]} )
Lemma: mFOLRule_ind_wf_simple
∀[A:Type]. ∀[v:mFOLRule()]. ∀[andI,impI:A]. ∀[allI,existsI:var:ℤ ─→ A]. ∀[orI:left:𝔹 ─→ A]. ∀[hyp:A].
∀[andE,orE,impE:hypnum:ℕ ─→ A]. ∀[allE,existsE:hypnum:ℕ ─→ var:ℤ ─→ A].
(mFOLRule_ind(v;
andI;
impI;
var.allI[var];
var.existsI[var];
left.orI[left];
hyp;hypnum.andE[hypnum];
hypnum.orE[hypnum];
hypnum.impE[hypnum];
hypnum,var.allE[hypnum;var];
hypnum,var.existsE[hypnum;var]) ∈ A)
Definition: mFOL-sequent
A sequent for mFOL is a list of hypothesis and a conclusion.⋅
mFOL-sequent() == mFOL() List × mFOL()
Lemma: mFOL-sequent_wf
mFOL-sequent() ∈ Type
Definition: mk_mFOLSequent
hyps⊢ concl == <hyps, concl>
Lemma: mk_mFOLSequent_wf
∀[hyps:mFOL() List]. ∀[concl:mFOL()]. (hyps⊢ concl ∈ mFOL-sequent())
Definition: mFOL-sequent-abstract
The abstract meaning of a sequent is a function
from the tuple of abstract meanings of the hypotheses to
the abstract meaning of the conclusion.⋅
mFOL-sequent-abstract(s) ==
let hyps,concl = s
in λDom,S,a. (tuple-type(map(λh.Dom,S,a |= mFOL-abstract(h);hyps)) ─→ Dom,S,a |= mFOL-abstract(concl))
Lemma: mFOL-sequent-abstract_wf
∀[s:mFOL-sequent()]. (mFOL-sequent-abstract(s) ∈ AbstractFOFormula)
Definition: mFOL-sequent-evidence
mFOL-sequent-evidence(s) == mFO-uniform-evidence{i:l}(mFOL-sequent-abstract(s))
Lemma: mFOL-sequent-evidence_wf
∀[s:mFOL-sequent()]. (mFOL-sequent-evidence(s) ∈ 𝕌')
Lemma: mFOL-sequent-evidence-trivial
Uniform evidence for a trivially true sequent where the conclusion is
a given member of the hypotheses.⋅
∀hyps:mFOL() List. ∀i:ℕ||hyps||. mFOL-sequent-evidence(<hyps, hyps[i]>)
Lemma: mFOL-sequent-evidence_transitivity1
From uniform evidence that hyps ⇒ x and uniform evidence that x ⇒ y
we construct uniform evidence that hyps ⇒ y.⋅
∀[hyps:mFOL() List]. ∀[x,y:mFOL()].
((∀[Dom:Type]. ∀[S:FOStruct(Dom)].
∀a:FOAssignment(Dom). (Dom,S,a |= mFOL-abstract(x) ⇒ Dom,S,a |= mFOL-abstract(y)))
⇒ mFOL-sequent-evidence(<hyps, x>)
⇒ mFOL-sequent-evidence(<hyps, y>))
Lemma: mFOL-sequent-evidence_transitivity2
From uniform evidence that hyps ⇒ y and
uniform evidence that (y ∧ hyps) ⇒ x
we construct uniform evidence that hyps ⇒ x.⋅
∀hyps:mFOL() List. ∀[x,y:mFOL()]. (mFOL-sequent-evidence(<hyps, y>) ⇒ mFOL-sequent-evidence(<[y / hyps], x>) ⇒ mFOL-s\000Cequent-evidence(<hyps, x>))
Lemma: mFOL-sequent-evidence_and
From uniform evidence that hyps ⇒ x and
uniform evidence that (y ∧ hyps) ⇒ y
we construct uniform evidence that hyps ⇒ x ∧ y⋅
∀hyps:mFOL() List. ∀[x,y:mFOL()]. (mFOL-sequent-evidence(<hyps, x>) ⇒ mFOL-sequent-evidence(<hyps, y>) ⇒ mFOL-sequent\000C-evidence(<hyps, x ∧ y>))
Definition: mFOLeffect
The effect of a given rule r on a given mFOL sequent s.
If the rule does not apply, then it `fails` by producing the effect ⌈inr ⋅ ⌉
otherwise it succeeds and produces ⌈inl L⌉where L is the list of subgoal sequents.⋅
mFOLeffect(sr) ==
let s,r = sr
in let hyps,concl = s
in mFOLRule_ind(r;
let a,b = dest-"and"(concl) in
inl [<hyps, a>; <hyps, b>];
let a,b = dest-"imp"(concl) in
inl [<[a / hyps], b>];
v.if (∀h∈hyps.¬bv ∈b mFOL-freevars(h)))_b ∧b (¬bv ∈b mFOL-freevars(concl)))
then let x,b = dest-all(concl); in
inl [<hyps, b[v/x]>]
else inr ⋅
fi ;
v.let x,b = dest-exists(concl); in
inl [<hyps, b[v/x]>];
x.let a,b = dest-"or"(concl) in
inl [<hyps, if x then a else b fi >];
if concl ∈b hyps) then inl [] else inr ⋅ fi ;i.if i <z ||hyps||
then let a,b = dest-"and"(hyps[i]) in
inl [<[a; [b / hyps]], concl>]
else inr ⋅
fi ;
i.if i <z ||hyps|| then let a,b = dest-"or"(hyps[i]) in inl [<[a / hyps], concl>; <[b / hyps], concl>] else inr \000C⋅ fi ;
i.if i <z ||hyps|| then let a,b = dest-"imp"(hyps[i]) in inl [<hyps, a>; <[b / hyps], concl>] else inr ⋅ fi ;
i,v.if i <z ||hyps|| then let x,b = dest-all(hyps[i]); in inl [<[b[v/x] / hyps], concl>] else inr ⋅ fi ;
i,v.if i <z ||hyps|| ∧b (∀h∈hyps.¬bv ∈b mFOL-freevars(h)))_b ∧b (¬bv ∈b mFOL-freevars(concl)))
then let x,b = dest-exists(hyps[i]); in
inl [<[b[v/x] / hyps], concl>]
else inr ⋅
fi )
Lemma: mFOLeffect_wf
∀[sr:mFOL-sequent() × mFOLRule()]. (mFOLeffect(sr) ∈ mFOL-sequent() List?)
Definition: mk_mFOLSequentRule
sBY r == <s, r>
Lemma: mk_mFOLSequentRule_wf
∀[s:mFOL-sequent()]. ∀[r:mFOLRule()]. (sBY r ∈ mFOL-sequent() × mFOLRule())
Definition: mk_mFOLProofNode
srsubgoals == <sr, subgoals>
Lemma: mk_mFOLProofNode_wf
∀[T:Type]. ∀[sr:mFOL-sequent() × mFOLRule()]. ∀[subgoals:T List]. (srsubgoals ∈ mFOL-sequent() × mFOLRule() × (T List))
Definition: mFOL-proveable
Provability of mFOL() sequent s.⋅
mFOL-proveable(s) == proveable(mFOL-sequent();mFOLRule();λsr.mFOLeffect(sr);s)
Lemma: mFOL-proveable_wf
∀[s:mFOL-sequent()]. (mFOL-proveable(s) ∈ ℙ)
Definition: mFOL-proveable-formula
mFOL-proveable-formula(fmla) == mFOL-proveable(<[], fmla>)
Lemma: mFOL-proveable-formula_wf
∀[fmla:mFOL()]. (mFOL-proveable-formula(fmla) ∈ ℙ)
Lemma: mFOL-proveable-evidence
Soundness theorem for mFOL() with respect to uniform evidence semantics.
It says that from a correct proof of a mFOL sequent we may construct
uniform evidence mFOL-sequent-evidence for the sequent.
Uniform evidence for an abstract formula, fmla, is the
intersection over all domains, Dom, and all structures, S, over Dom,
of evidence for ∀a:FOAssignment(Dom). Dom,S,a |= fmla.
NOTE:
Since there are no assignments into an empty domain, this means that any
evidence works when Dom is empty, so the intersection is essentially over
non-empty domains Dom.
Thus, (forall x. P(x)) => (exists x. P(x)) is uniformly valid
(i.e. has uniform evidence) so (by our completeness theorem) is provable.
A careful examination of the effect of the mFOL rules
(see mFOLeffect)
will show that it is indeed provable.⋅
∀[s:mFOL-sequent()]. (mFOL-proveable(s) ⇒ mFOL-sequent-evidence(s))
Lemma: mFOL-proveable-formula-evidence
Main Lemma. See mFOL-proveable-evidence also.⋅
∀[fmla:mFOL()]. (mFOL-proveable-formula(fmla) ⇒ mFOL-evidence(fmla))
Lemma: mFOL-proveable-formula-evidence-ext
Main Lemma. See mFOL-proveable-evidence also.⋅
∀[fmla:mFOL()]. (mFOL-proveable-formula(fmla) ⇒ mFOL-evidence(fmla))
Lemma: mFOL-proveable-formula-evidence-ext2
Main Lemma. See mFOL-proveable-evidence also.⋅
∀[fmla:mFOL()]. (mFOL-proveable-formula(fmla) ⇒ mFOL-evidence(fmla))
Definition: new-mFO-var
new-mFO-var(H) ==
accumulate (with value m and list item fmla):
let vs ←─ mFOL-freevars(fmla)
in eval n = bigger-int(m;vs) in
n
over list:
H
with starting value:
0)
Lemma: new-mFO-var_wf
∀[H:mFOL() List]. (new-mFO-var(H) ∈ ℤ)
Definition: compute-in-context
compute-in-context(constants;functions;t) ==
fix((λcompute-in-context,t. (if t is stopped at f,n then
case apply-alist(IntDeq;constants;n)
of inl(x) =>
compute-in-context (f x)
| inr(z) =>
case apply-alist(IntDeq;functions;n)
of inl(table) =>
(if f (λx.stop(x)) is stopped at g,arg then
if compute-in-context arg is an integer
case apply-alist(IntDeq;table;compute-in-context arg)
of inl(z) =>
compute-in-context (f (λx.z))
| inr(z) =>
t
else t
otherwise x.t)
| inr(z) =>
t
otherwise x.x)))
t
Definition: elimination-step
elimination-step(H;eliminated;model;f;n) ==
fix((λelimination-step,f,n. mFOL_ind(H[||H|| - n + 1];
mFOatomic(P,vars)⇒ "stopped on a atomic hyp??";
mFOconnect(knd,A,B)⇒ a,b.if knd =a "imp"
then (if f (λx.stop(x)) is stopped at g,a then
<n, a>
otherwise x.<n, "stopped on implies not applied??">)
else <n, 0>
fi ;
mFOquant(isall,v,body)⇒ r.if isall
then (if f (λx.stop(x)) is stopped at h,a then
(if compute-in-context(eliminated;model;a) is stopped at g,m then
elimination-step g m
otherwise b.<n, b>)
otherwise x.<n, "stopped on all not applied??">)
else <n, 0>
fi ) ))
f
n
Definition: do-elimination-step
do-elimination-step(H; G; eliminated; model; evd; f; n) ==
let incurrent = λe.<e, eliminated, model> in
let m,a = elimination-step(H;eliminated;model;f;n)
in let eliminate = λt.<evd, [<m, t> / eliminated], model> in
eval k = ||H|| in
eval hnum = k - m + 1 in
eval hyp = H[hnum] in
mFOL_ind(hyp;
mFOatomic(P,vars)⇒ "stopped on a atomic hyp??";
mFOconnect(knd,A,B)⇒ _,__.if knd =a "imp"
then <impE on hnum, [incurrent a; eliminate (λx.stop(k))]>
if knd =a "and" then <andE on hnum, [eliminate <stop(k + 1), stop(k)>]>
if knd =a "or" then <orE on hnum, [eliminate (inl stop(k)); eliminate (inr stop(k) )]>
else "funny connective??"
fi ;
mFOquant(isall,v,body)⇒ _.if isall
then eval model' = update-alist(IntDeq;model;m;[<a, stop(k)>];table.[<a, stop(k)> / table]) in
<allE on hnum with a, [<evd, eliminated, model'>]>
else eval j = new-mFO-var([G / H]) in
<existsE on hnum with j, [eliminate <j, stop(k)>]>
fi )
Definition: full-evd-proof-step
full-evd-proof-step:
sequent;
fullevd ==
let H,G = sequent
in let evd,eliminated,model = fullevd in
(if compute-in-context(eliminated;model;evd) is stopped at f,n then
if eq_term(f; λx.x) then <hyp, []> else do-elimination-step(H; G; eliminated; model; evd; f; n) fi
otherwise evd.let incurrent = λe.<e, eliminated, model> in
if evd is a pair
then let left,right = evd
in if mFOconnect?(G) ∧b mFOconnect-knd(G) =a "and"
then <andI, [incurrent left; incurrent right]>
else (if compute-in-context(eliminated;model;left) is stopped at f,n then
do-elimination-step(H; G; eliminated; model; evd; f; n)
otherwise w.<existsI with w, [incurrent right]>)
fi otherwise if evd is lambda then if mFOconnect?(G) ∧b mFOconnect-knd(G) =a "imp"
then eval k = ||H|| in
<impI, [incurrent (evd stop(k))]>
else eval m = new-mFO-var(H) in
<allI with new-mFO-var(H), [incurrent (evd m)]>
fi otherwise if evd is inl then <orI left, [incurrent outl(evd)]>
else if evd is inr then <orI right, [incurrent outr(evd)]>
else "can't happen if evd is correct")
Definition: uniform-evd-proof-checks
uniform-evd-proof-checks(sequent;fullevd) ==
fix((λuniform-evd-proof-checks,sequent,fullevd. let rule,subevd = full-evd-proof-step:
sequent;
fullevd
in let sr ←─ <sequent, rule>
in case mFOLeffect(sr)
of inl(L) =>
let subgoals ←─ L
in eval n = ||subgoals|| in
(∀i∈upto(n).uniform-evd-proof-checks subgoals[i] subevd[i])_b
| inr(z) =>
ff))
sequent
fullevd
Definition: uniform-evd-proof
uniform-evd-proof(sequent;fullevd) ==
fix((λuniform-evd-proof,sequent,fullevd. let rule,subevd = full-evd-proof-step:
sequent;
fullevd
in let sr ←─ <sequent, rule>
in let subgoals ←─ outl(mFOLeffect(sr))
in eval n = ||subgoals|| in
<sr, map(λi.(uniform-evd-proof subgoals[i] subevd[i]);upto(n))>))
sequent
fullevd
Definition: mfol-context
This is the list of hypotheses of a mFOL-sequent() in reverse order.⋅
mfol-context() == mFOL() List
Lemma: mfol-context_wf
mfol-context() ∈ Type
Definition: mfol-context-model
A pair <consts,funs> where consts is an association list that can assign
number n a triple such as ⌈<"pair", i, j>⌉.
funs is an association list of type ⌈(ℤ × ((ℤ × ℤ) List)) List⌉.
It can assign to number n a secondary association list.
So if 0 is assigned the list [<1,4>;<2;5>] it means that
0 is a function that maps domain element 1 to hypothesis 4 and
domain element 2 to hypothesis 5⋅
mfol-context-model() == (ℤ × Atom × ℤ × ℤ) List × ((ℤ × ((ℤ × ℤ) List)) List)
Lemma: mfol-context-model_wf
mfol-context-model() ∈ Type
Definition: modelEval
modelEval(exname;M;n)
==r let consts,funs = M
in case apply-alist(IntDeq;funs;n)
of inl(lst) =>
λi.if i is an integer then case apply-alist(IntDeq;lst;i)
of inl(j) =>
modelEval(exname;M;j)
| inr(x) =>
exception(<exname, n, i>)
else exception(<exname, n, i>)
| inr(x) =>
case apply-alist(IntDeq;consts;n)
of inl(x) =>
let lbl,i,j = x in
if lbl =a "function" then λx.exception(<exname, n, x>)
if lbl =a "pair" then <modelEval(exname;M;i), modelEval(exname;M;j)>
if lbl =a "dpair" then <i, modelEval(exname;M;j)>
if lbl =a "inl" then inl modelEval(exname;M;i)
if lbl =a "inr" then inr modelEval(exname;M;i)
if lbl =a "const" then λx.modelEval(exname;M;i)
else exception(<exname, n>)
fi
| inr(x) =>
exception(<exname, n>)
Definition: modelAdd
M[n:= lbl,i,j] == let consts,funs = M in <update-alist(IntDeq;consts;n;<lbl, i, j>;tr.<lbl, i, j>), funs>
Definition: modelUpdate
M[fnum(x) :=n] == let consts,funs = M in <consts, update-alist(IntDeq;funs;fnum;[<x, n>];l.[<x, n> / l])>
Definition: note-is-function
note-is-function(A;hnum;M) == if mFOLisImp(A) ∨bmFOLisAll(A) then M[hnum:= `function`] else M fi
Definition: ex-do-Intro
ex-do-Intro(exname; H; G; numhyps; val; fullevd) ==
let F,M = fullevd
in mFOL_ind(G;
mFOatomic(P,vars)⇒ "should not happen??";
mFOconnect(knd,A,B)⇒ _,__.if knd =a "imp"
then let M' ←─ note-is-function(A;numhyps;M)
in <impI, [<λM.(F M modelEval(exname;M;numhyps)), M'>]>
if knd =a "and" then <andI, [<λM.(fst((F M))), M>; <λM.(snd((F M))), M>]>
if knd =a "or"
then case val of inl(_) => <orI left, [<λM.outl(F M), M>]> | inr(_) => <orI right, [<λM.outr(F M), M>]>
else "funny connective??"
fi ;
mFOquant(isall,v,body)⇒ _.if isall
then eval m = new-mFO-var(H) in
<allI with m, [<λM.(F M m), M>]>
else eval j = fst(val) in
<existsI with j, [<λM.(snd((F M))), M>]>
fi )
Definition: ex-do-Elim
ex-do-Elim(exname;H;G;numhyps;m';fullevd)
==r let F,M = fullevd
in eval m = if m' is a pair then fst(m') otherwise m' in
eval hnum = numhyps - m + 1 in
eval hyp = H[hnum] in
mFOL_ind(hyp;
mFOatomic(P,vars)⇒ <hyp, []>;
mFOconnect(knd,A,B)⇒ _,__.if knd =a "imp"
then let M' ←─ note-is-function(B;numhyps;M[m:= λx.numhyps])
in <impE on hnum
, [<λM.F M?exname:e.if e is a pair then let a,b = e
in if (a =z m)
then b
else exception(<exname
, e
>)
fi
otherwise exception(<exname, e>)
, M
>;
<F, M'>]
>
if knd =a "and"
then let M' ←─ note-is-function(A;numhyps + 1;note-is-function(B;numhyps;M[m:= <numhyps
+ 1,numhyps>]))
in <andE on hnum, [<F, M'>]>
if knd =a "or"
then let M1 ←─ note-is-function(A;numhyps;M[m:= inl(numhyps)])
in let M2 ←─ note-is-function(B;numhyps;M[m:= inr(numhyps)])
in <orE on hnum, [<F, M1>; <F, M2>]>
else "funny connective??"
fi ;
mFOquant(isall,v,body)⇒ _.if isall
then eval a = snd(m') in
let M' ←─ note-is-function(body;numhyps;M[m(a) :=numhyps])
in <allE on hnum with a, [<F, M'>]>?exname:m'.ex-do-Elim(exname;H;G;numhyps;m';fullevd)
else eval j = new-mFO-var([G / H]) in
let M' ←─ note-is-function(body;numhyps;M[m:= <dj,numhyps>])
in <existsE on hnum with j, [<F, M'>]>
fi )
Definition: ex-evd-proof-step
ex-evd-proof-step(exname; sequent; fullevd) ==
let H,G = sequent
in eval numhyps = ||H|| in
let F,M = fullevd
in eval v = F M in
ex-do-Intro(exname; H; G; numhyps; v; fullevd)?exname:n.ex-do-Elim(exname;H;G;numhyps;n;fullevd)
Definition: ex-evd-proof
ex-evd-proof(exname;sequent;F)
==r let rule,subevd = ex-evd-proof-step(exname; sequent; F)
in let sr ←─ <sequent, rule>
in let subgoals ←─ outl(mFOLeffect(sr))
in eval n = ||subgoals|| in
<sr, map(λi.ex-evd-proof(exname;subgoals[i];subevd[i]);upto(n))>
Definition: ex-evd-proof-check
ex-evd-proof-check(exname;sequent;F)
==r let rule,subevd = ex-evd-proof-step(exname; sequent; F)
in let sr ←─ <sequent, rule>
in case mFOLeffect(sr)
of inl(subgoals) =>
eval n = ||subgoals|| in
(∀i∈upto(n).ex-evd-proof-check(exname;subgoals[i];subevd[i]))_b
| inr(z) =>
ff
Definition: uniform-evd-to-proof
uniform-evd-to-proof(G;evd) == evalall(ν(ex.ex-evd-proof(ex;<[], G>;<λM.evd, [], []>)))
Definition: uniform-evd-proof-check
uniform-evd-proof-check(exname; fmla; evd) == evalall(ex-evd-proof-check(exname;<[], fmla>;<λM.evd, [], []>))
Comment: the proof algorithm
Starting with evidence evd of formula G, we form sequent ⌈<[], G>⌉
and "full evidence" ⌈<λM.evd, [], []>⌉ consisting of function F = ⌈λM.evd⌉
and the empty model M = <[], []>.
We also need a name ⌈exname⌉ that is fresh w.r.t. the evidence (i.e. not mentioned in evd).
uniform-evd-to-proof(exname; G; evd) == evalall(ex-evd-proof(exname;<[], G>;<λM.evd, [], []>))
To generate the proof of a sequent from its full evidence, we generate the next step
consisting of the proof rule to apply and a list of full evidence for the subgoals.
The minimal-first-order-logic proof system defines the effect of the rule r on sequent s
as either ⌈inl subgoals⌉ or ⌈inr Ax ⌉ where the rule succeeds when we get ⌈inl subgoals⌉.
So we build the proof tree by putting in the sequent and rule and the list of subproofs
generated by pairing up the subgoal sequents with the sub-evidence.
ex-evd-proof(exname;sequent;fullevd)
==r let rule,subevd = ex-evd-proof-step(exname; sequent; fullevd)
in let sr ←─ <sequent, rule>
in let subgoals ←─ outl(mFOLeffect(sr))
in eval n = ||subgoals|| in
<sr, map(λi.ex-evd-proof(subgoals[i]; subevd[i]);upto(n))>
To generate the next step apply the function F to the model M.
If we get a value, do an introduction rule,
if an exception is raised
(either when F is applied to M, or when computing the introduction rule),
then catch that exception and do an elimination step.
ex-evd-proof-step(exname; sequent; fullevd) ==
let H,G = sequent
in eval numhyps = ||H|| in
let F,M = fullevd
in eval v = F M in
ex-do-Intro(exname; H; G; numhyps; v; fullevd)?exname:n.ex-do-Elim(exname;H;G;numhyps;n;fullevd)
To do an introduction rule using the value, val, computed from the evidence,
do a case analysis on the conclusion G of the sequent.
The only case that adds a new hypothesis is implies introduction.
In that case, we update the model M when the new hypothesis A is a function
(a forall formula or an implies formula) to indicate that.
Otherwise the model M stays the same.
The function F that we apply to the model is updated so that it applies
the appropriate operation (e.g. fst, snd, outl, outr) to the previously computed (F M).
In the case of exists, we compute the first component of the pair, val.
If that raises an exception, then the introduction step will raise an exception and
the proof will do an elimination step instead.
Notice that the ImpliesIntroduction changes the function so that it applies the evidence to
another argument, modelEval(M,n), where n = numhyps is the number of
the newly introduced hypothesis.
The definition of modelEval is given below (at the end).
ex-do-Intro(H;G;numhyps;val;fullevd) ==
let F,M = fullevd
in mFOL_ind(G;
mFOatomic(P,vars)⇒ "should not happen??";
mFOconnect(knd,A,B)⇒ _,__.if knd =a "imp"
then let M' ←─ note-is-function(A;numhyps;M)
in <impI, [<λM.(F M modelEval(M; numhyps)), M'>]>
if knd =a "and" then <andI, [<λM.(fst((F M))), M>; <λM.(snd((F M))), M>]>
if knd =a "or"
then case val of inl(_) => <orI left, [<λM.outl(F M), M>]> | inr(_) => <orI right, [<λM.outr(F M), M>]>
else "funny connective??"
fi ;
mFOquant(isall,v,body)⇒ _.if isall
then eval m = new-mFO-var(H) in
<allI with m, [<λM.(F M m), M>]>
else eval j = fst(val) in
<existsI with j, [<λM.(snd((F M))), M>]>
fi )
Here is the definition of note-is-function:
note-is-function(A;hnum;M) == if mFOLisImp(A) ∨bmFOLisAll(A) then M[hnum:= `function`] else M fi
To do an elimination step using the exception m', we use the first
component m of m' when m' is a pair.
That is because when we evaluate hypothesis number m in a model that only
specifies that m is a function, then we use ⌈λx.exception(<exname, m, x>)⌉
for the meaning of m. That will raise a (named) exception with value part
⌈<m, x>⌉ if the function is applied to term ⌈x⌉ in a principal part
of the computation, and we will
know that hypothesis m needs elimination and that it was applied to term x.
From m, we get the hypothesis on which to apply the elimination rule (the hypotheses are listed in
reverse H(numhyps-1),...., H2, H1, H0 ) and do case analysis on that hypothesis.
In most cases, in the evidence for the generated subgoal(s),
the function F in the full evidence stays the same, and the model is updated.
The model is updated to indicate that, for example, an "and" hypothesis is equal to the
pair of new hypotheses, or an "or" hypothesis is equal to inl or inr of the new hypothesis.
In every case that adds a new hypothesis, we use note-is-function to update the model when the
new hypothesis is a function.
The trickiest case is the evidence for the first subgoal of implies-elimination.
In that case we know that the computation (F M) raises exception ⌈<m, x>⌉ so we change the
function so that it catches exceptions and when the exception has the form ⌈<m, x>⌉ it continues
using evidence x. It re-raises any other exceptions.
The other tricky case is forall-elimination.
In that case, since a forall is a function,
the exception m' must be a pair, and the second component
is the domain element to be instantiated.
So we try to compute that to a value.
If an exception is raised, then we use that to compute the
next step instead.
Because of that possibilty, the function ex-do-Elim is recursive.
%---%
ex-do-Elim(exname;H;G;numhyps;m';fullevd)
==r let F,M = fullevd
in eval m = if m' is a pair then fst(m') otherwise m' in
eval hnum = numhyps - m + 1 in
eval hyp = H[hnum] in
mFOL_ind(hyp;
mFOatomic(P,vars)⇒ <hyp, []>;
mFOconnect(knd,A,B)⇒ _,__.if knd =a "imp"
then let M' ←─ note-is-function(B;numhyps;M[m:= λx.numhyps])
in <impE on hnum
, [<λM.F M?exname:e.if e is a pair then let a,b = e
in if (a =z m)
then b
else exception(<exname
, e
>)
fi
otherwise exception(<exname, e>)
, M
>;
<F, M'>]
>
if knd =a "and"
then let M' ←─ note-is-function(A;numhyps + 1;note-is-function(B;numhyps;M[m:= <numhyps
+ 1,numhyps>]))
in <andE on hnum, [<F, M'>]>
if knd =a "or"
then let M1 ←─ note-is-function(A;numhyps;M[m:= inl(numhyps)])
in let M2 ←─ note-is-function(B;numhyps;M[m:= inr(numhyps)])
in <orE on hnum, [<F, M1>; <F, M2>]>
else "funny connective??"
fi ;
mFOquant(isall,v,body)⇒ _.if isall
then eval a = snd(m') in
let M' ←─ note-is-function(body;numhyps;M[m(a) :=numhyps])
in <allE on hnum with a, [<F, M'>]>?exname:m'.ex-do-Elim(exname;H;G;numhyps;m';fullevd)
else eval j = new-mFO-var([G / H]) in
let M' ←─ note-is-function(body;numhyps;M[m:= <dj,numhyps>])
in <existsE on hnum with j, [<F, M'>]>
fi )
Finally, here is the recursive definition of modelEval(M,n):
M is a pair <consts,funs> where consts is an association list of type
⌈(ℤ × Atom × ℤ × ℤ) List⌉ that can assign to number n a triple such as ⌈<"pair", i, j>⌉.
funs is an association list of type ⌈(ℤ × ((ℤ × ℤ) List)) List⌉. It can assign to number n
a secondary association list. So if 0 is assigned the list [<1,4>;<2;5>] it means that
0 is a function that maps domain element 1 to hypothesis 4 and domain element 2 to hypothesis 5.
modelEval(exname;M;n)
==r let consts,funs = M
in case apply-alist(IntDeq;funs;n)
of inl(lst) =>
λi.if i is an integer then case apply-alist(IntDeq;lst;i)
of inl(j) =>
modelEval(exname;M;j)
| inr(x) =>
exception(<exname, n, i>)
else exception(<exname, n, i>)
| inr(x) =>
case apply-alist(IntDeq;consts;n)
of inl(x) =>
let lbl,i,j = x in
if lbl =a "function" then λx.exception(<exname, n, x>)
if lbl =a "pair" then <modelEval(exname;M;i), modelEval(exname;M;j)>
if lbl =a "dpair" then <i, modelEval(exname;M;j)>
if lbl =a "inl" then inl modelEval(exname;M;i)
if lbl =a "inr" then inr modelEval(exname;M;i)
if lbl =a "const" then λx.modelEval(exname;M;i)
else exception(<exname, n>)
fi
| inr(x) =>
exception(<exname, n>)⋅
Home
Index