| CARVIEW |
Select Language
HTTP/2 200
date: Thu, 15 Jan 2026 22:44:29 GMT
content-type: text/html; charset=UTF-8
server: cloudflare
x-frame-options: DENY
x-content-type-options: nosniff
x-xss-protection: 1;mode=block
set-cookie: _csrf-frontend=9f06ebbe041b7c7594ce67a21107d049ceac537cc346961da9de42b05d0f4cc0a%3A2%3A%7Bi%3A0%3Bs%3A14%3A%22_csrf-frontend%22%3Bi%3A1%3Bs%3A32%3A%22riLxmhb-dD3CBiFLVi9t8kCRT0K1SgJK%22%3B%7D; path=/; HttpOnly
vary: accept-encoding
cf-cache-status: DYNAMIC
content-encoding: gzip
cf-ray: 9be8e5e2fedaa9c3-BLR
Smullyan Incompleteness - Pastebin.com
SHARE
TWEET
Smullyan Incompleteness
a guest
Apr 2nd, 2015
2,698
0
Never
Add comment
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- (*see https://blog.plover.com/math/Gdl-Smullyan.html*)
- Inductive Token :=
- |P : Token
- |PR : Token
- |N : Token.
- Inductive Formula :=
- |T : Formula (*empty string*)
- |l_app : Token -> Formula -> Formula.
- Fixpoint concat(F F':Formula) :=
- match F with
- |T => F'
- |(l_app t F'') => l_app t (concat F'' F')
- end.
- Infix "+" := l_app.
- Infix "++" := concat.
- Variable Printed : Formula -> Prop. (*set of formulas printed by computer*)
- Fixpoint Truth(F:Formula):Prop := (*semantics*)
- match F with
- |T => True
- |(P+F') => Printed(F')
- |(PR+F') => Printed(F'++F')
- |(N+F') => ~Truth(F')
- end.
- Definition Consistent := forall F:Formula, Printed F -> Truth F.
- Definition Complete := forall F:Formula, Truth F -> Printed F.
- Lemma Incompleteness : ~(Consistent /\ Complete).
- Proof.
- unfold Complete, Consistent.
- intro.
- destruct H as [Cons Comp].
- assert (~Printed (N+(PR+(N+(PR+T))))).
- intro.
- assert (Truth (N+(PR+(N+(PR+T))))).
- apply Cons.
- exact H.
- simpl in H0.
- contradiction.
- assert (Printed (N + (PR + (N + (PR + T))))).
- apply Comp.
- simpl.
- exact H.
- contradiction.
- Qed.
Advertisement
Add Comment
Please, Sign In to add comment
-
✅ Method to get 13,000$ in 2 days
CSS | 42 min ago | 0.94 KB
-
Crypto Exploit
42 min ago | 0.94 KB
-
Untitled
2 hours ago | 18.19 KB
-
Untitled
4 hours ago | 15.61 KB
-
Untitled
HTML | 5 hours ago | 9.80 KB
-
Untitled
6 hours ago | 6.46 KB
-
Untitled
8 hours ago | 18.60 KB
-
Untitled
10 hours ago | 12.84 KB
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
