:: G{\"o}del's Completeness Theorem
:: by Patrick Braselmann and Peter Koepke
::
:: Received September 25, 2004
:: Copyright (c) 2004 Association of Mizar Users
:: deftheorem Def1 defines negation_faithful GOEDELCP:def 1 :
:: deftheorem Def2 defines with_examples GOEDELCP:def 2 :
theorem :: GOEDELCP:1
theorem Th2: :: GOEDELCP:2
theorem Th3: :: GOEDELCP:3
theorem :: GOEDELCP:4
theorem Th5: :: GOEDELCP:5
theorem Th6: :: GOEDELCP:6
theorem :: GOEDELCP:7
theorem Th8: :: GOEDELCP:8
theorem Th9: :: GOEDELCP:9
theorem Th10: :: GOEDELCP:10
theorem Th11: :: GOEDELCP:11
theorem Th12: :: GOEDELCP:12
theorem :: GOEDELCP:13
theorem Th14: :: GOEDELCP:14
theorem Th15: :: GOEDELCP:15
theorem Th16: :: GOEDELCP:16
theorem Th17: :: GOEDELCP:17
theorem Th18: :: GOEDELCP:18
:: deftheorem Def3 defines ExCl GOEDELCP:def 3 :
theorem Th19: :: GOEDELCP:19
theorem Th20: :: GOEDELCP:20
Lm1:
for A being non empty set st A is countable holds
ex f being Function st
( dom f = NAT & A = rng f )
:: deftheorem Def4 defines Ex-bound_in GOEDELCP:def 4 :
:: deftheorem Def5 defines Ex-the_scope_of GOEDELCP:def 5 :
:: deftheorem Def6 defines bound_in GOEDELCP:def 6 :
:: deftheorem Def7 defines the_scope_of GOEDELCP:def 7 :
:: deftheorem defines still_not-bound_in GOEDELCP:def 8 :
theorem Th21: :: GOEDELCP:21
theorem Th22: :: GOEDELCP:22
theorem Th23: :: GOEDELCP:23
theorem Th24: :: GOEDELCP:24
theorem Th25: :: GOEDELCP:25
theorem Th26: :: GOEDELCP:26
theorem Th27: :: GOEDELCP:27
theorem Th28: :: GOEDELCP:28
theorem Th29: :: GOEDELCP:29
theorem Th30: :: GOEDELCP:30
theorem Th31: :: GOEDELCP:31
theorem Th32: :: GOEDELCP:32
theorem Th33: :: GOEDELCP:33
theorem Th34: :: GOEDELCP:34
theorem Th35: :: GOEDELCP:35
theorem Th36: :: GOEDELCP:36
theorem Th37: :: GOEDELCP:37
theorem :: GOEDELCP:38