:: Equivalences of Inconsistency and {H}enkin Models
:: by Patrick Braselmann and Peter Koepke
::
:: Received September 25, 2004
:: Copyright (c) 2004-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, CQC_LANG, QC_LANG1, FINSEQ_1, XBOOLE_0,
FINSET_1, FUNCT_1, ORDINAL1, RELAT_1, ARYTM_3, TARSKI, WELLORD2,
WELLORD1, CARD_1, NAT_1, CQC_THE1, ORDINAL4, XBOOLEAN, CALCUL_1,
CALCUL_2, ARYTM_1, INT_1, XXREAL_0, FUNCT_2, ZFMISC_1, VALUAT_1,
ZF_MODEL, MARGREL1, REALSET1, MCART_1, HENMODEL;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, CALCUL_1, RELAT_1,
FUNCT_1, ORDINAL1, XCMPLX_0, XXREAL_0, INT_1, NAT_1, FINSEQ_1, QC_LANG1,
CQC_LANG, CQC_THE1, VALUAT_1, FINSET_1, RELSET_1, FUNCT_2, CARD_1,
MARGREL1, CQC_SIM1, DOMAIN_1, XTUPLE_0, MCART_1, NUMBERS, FINSEQ_3,
CALCUL_2, WELLORD1, WELLORD2;
constructors SETFAM_1, WELLORD1, WELLORD2, DOMAIN_1, XXREAL_0, NAT_1, INT_1,
FINSEQ_3, CQC_SIM1, SUBSTUT2, CALCUL_1, CALCUL_2, RELSET_1, XTUPLE_0,
NUMBERS;
registrations SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, FINSET_1, XXREAL_0,
XREAL_0, INT_1, FINSEQ_1, QC_LANG1, CQC_LANG, FINSEQ_2, CARD_1, XTUPLE_0,
FUNCT_2;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
begin :: Preliminaries and Equivalences of Inconsistency
reserve Al for QC-alphabet;
reserve a,a1,a2,b,c,d for set,
X,Y,Z for Subset of CQC-WFF(Al),
i,k,m,n for Nat,
p,q for Element of CQC-WFF(Al),
P for QC-pred_symbol of k,Al,
ll for CQC-variable_list of k,Al,
f,f1,f2,g for FinSequence of CQC-WFF(Al);
reserve A for non empty finite Subset of NAT;
theorem :: HENMODEL:1
for f being Function of n,A st ((ex m st succ m = n) & rng f = A
& for n,m st m in dom f & n in dom f & n < m holds f.n in f.m) holds f.(union n
) = union rng f;
theorem :: HENMODEL:2
union A in A & for a st a in A holds (a in union A or a = union A );
reserve C for non empty set;
theorem :: HENMODEL:3
for f being sequence of C, X being finite set st (for n,m st
m in dom f & n in dom f & n < m holds f.n c= f.m) & X c= union rng f holds ex k
st X c= f.k;
definition
let Al;
let X,p;
pred X |- p means
:: HENMODEL:def 1
ex f st rng f c= X & |- f^<*p*>;
end;
definition
let Al;
let X;
attr X is Consistent means
:: HENMODEL:def 2
for p holds not (X |- p & X |- 'not' p);
end;
notation
let Al;
let X;
antonym X is Inconsistent for X is Consistent;
end;
definition
let Al;
let f be FinSequence of CQC-WFF(Al);
attr f is Consistent means
:: HENMODEL:def 3
for p holds not (|- f^<*p*> & |- f^<*'not' p*>);
end;
notation
let Al;
let f be FinSequence of CQC-WFF(Al);
antonym f is Inconsistent for f is Consistent;
end;
theorem :: HENMODEL:4
X is Consistent & rng g c= X implies g is Consistent;
theorem :: HENMODEL:5
|- f^<*p*> implies |- f^g^<*p*>;
:: Ebb et al, Chapter IV, Lemma 7.2
theorem :: HENMODEL:6
X is Inconsistent iff for p holds X |- p;
:: One direction of Ebb et al, Chapter IV, Lemma 7.4
theorem :: HENMODEL:7
X is Inconsistent implies ex Y st Y c= X & Y is finite & Y is Inconsistent;
theorem :: HENMODEL:8
X \/ {p} |- q implies ex g st rng g c= X & |- g^<*p*>^<*q*>;
:: Corresponds to Ebb et al, Chapter IV, Lemma 7.6 (a)
theorem :: HENMODEL:9
X |- p iff X \/ {'not' p} is Inconsistent;
:: Similar to Ebb et al, Chapter IV, Lemma 7.6 (a)
theorem :: HENMODEL:10
X |- 'not' p iff X \/ {p} is Inconsistent;
begin :: Unions of Consistent Sets
:: Ebb et al, Chapter IV, Lemma 7.7
theorem :: HENMODEL:11
for f being sequence of bool CQC-WFF(Al) st (for n,m st m in dom f & n
in dom f & n < m holds f.n is Consistent & f.n c= f.m) holds (union rng f) is
Consistent;
begin :: Construction of a Henkin Model
reserve A for non empty set,
v for Element of Valuations_in(Al,A),
J for interpretation of Al,A;
theorem :: HENMODEL:12
X is Inconsistent implies for J,v holds not J,v |= X;
theorem :: HENMODEL:13
{VERUM(Al)} is Consistent;
registration
let Al;
cluster Consistent for Subset of CQC-WFF(Al);
end;
reserve CX for Consistent Subset of CQC-WFF(Al),
P9 for Element of QC-pred_symbols(Al);
definition
let Al;
func HCar(Al) -> non empty set equals
:: HENMODEL:def 4
bound_QC-variables(Al);
end;
definition
let Al;
let P be (Element of QC-pred_symbols(Al)), ll be CQC-variable_list of (
the_arity_of P), Al;
redefine func P!ll -> Element of CQC-WFF(Al);
end;
:: The Henkin Model (Ebb et al, Chapter V, §1)
definition
let Al;
let CX;
mode Henkin_interpretation of CX -> interpretation of Al,HCar(Al) means
:: HENMODEL:def 5
for
P being (Element of QC-pred_symbols(Al)), r being Element of relations_on
HCar(Al) st it.P = r holds for a holds a in r iff
ex ll being CQC-variable_list of (the_arity_of P), Al st a = ll &
CX |- P!ll;
end;
definition
let Al;
func valH(Al) -> Element of Valuations_in (Al,HCar(Al)) equals
:: HENMODEL:def 6
id bound_QC-variables(Al);
end;
begin :: Some Properties of the Henkin Model
reserve JH for Henkin_interpretation of CX;
theorem :: HENMODEL:14
(valH(Al))*'ll = ll;
theorem :: HENMODEL:15
|- f^<*VERUM(Al)*>;
theorem :: HENMODEL:16
JH,valH(Al) |= VERUM(Al) iff CX |- VERUM(Al);
theorem :: HENMODEL:17
JH,valH(Al) |= P!ll iff CX |- P!ll;