:: Equivalences of Inconsistency and {H}enkin Models
:: by Patrick Braselmann and Peter Koepke
::
:: Received September 25, 2004
:: Copyright (c) 2004 Association of Mizar Users
theorem Th1: :: HENMODEL:1
theorem Th2: :: HENMODEL:2
theorem Th3: :: HENMODEL:3
:: deftheorem HENMODEL:def 1 :
canceled;
:: deftheorem Def2 defines |- HENMODEL:def 2 :
:: deftheorem Def3 defines Consistent HENMODEL:def 3 :
:: deftheorem Def4 defines Consistent HENMODEL:def 4 :
theorem Th4: :: HENMODEL:4
theorem Th5: :: HENMODEL:5
theorem Th6: :: HENMODEL:6
theorem Th7: :: HENMODEL:7
Lm1:
for f, g being FinSequence holds Seg (len (f ^ g)) = (Seg (len f)) \/ (seq (len f),(len g))
theorem :: HENMODEL:8
theorem :: HENMODEL:9
theorem :: HENMODEL:10
theorem :: HENMODEL:11
theorem Th12: :: HENMODEL:12
theorem Th13: :: HENMODEL:13
:: deftheorem defines HCar HENMODEL:def 5 :
:: deftheorem Def6 defines Henkin_interpretation HENMODEL:def 6 :
:: deftheorem defines valH HENMODEL:def 7 :
theorem Th14: :: HENMODEL:14
theorem Th15: :: HENMODEL:15
theorem :: HENMODEL:16
theorem :: HENMODEL:17