:: Equivalences of Inconsistency and {H}enkin Models
::  by Patrick Braselmann and Peter Koepke
::
:: Received September 25, 2004
:: Copyright (c) 2004-2021 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;