- Yes. $\neg (\mathbf{F}A) \equiv \mathbf{G}(\neg A)$ is true: it expresses the equivalence
of “It is not true that A will be true at some point in the future” and “It will always be
the case from now on that A is not true.” Furthermore, $\neg (\mathbf{G}A) \equiv \mathbf{F}(\neg A)$ is also true: it expresses the equivalence of “It is not true that A will be now and forever true” and “There will be some time in the future that A will be not true.”
- We are given that the system is bivalent, so every formula will have a truth value that is either true or false, exclusively. There are no other possibilities. Now let $G$ be the sentence “I am not provable.” We have two things to prove:
- Assume the system is consistent.
-
Assume $G$ is true.
$G$ says it is not provable.
This is a true statement that has no proof.
So in this case the system is incomplete. -
Assume $G$ is false.
Then the opposite of what it says is true, namely $G$ is provable.
So we have a proof of $G$.
Because of consistency, we must not have a proof of $\neg G$.
But $\neg G$ is true. And we have no proof of it. So again, the system is incomplete.
-
Assume $G$ is true.
- Assume the system is complete.
-
Assume $G$ is true.
$G$ says it is not provable.
But because we assumed completeness, we cannot have this!
Therefore $G$ must be false. -
So $G$ is false.
Then the opposite of what it says is true, namely $G$ is provable.
So we have a proof of $G$.
But we assumed completeness, so we have a proof of every true statement.
$\neg G$ is true, so we must have a proof of $\neg G$.
So we have a proof of both $G$ and $\neg G$.
So the system is inconsistent
-
Assume $G$ is true.
- Assume the system is consistent.
- Some grammars:
oddLenPal → "A" oddLenPal "A" | "B" oddLenPal "B" | "C" oddLenPal "C" | "D" oddLenPal "D" -- and so on, for each of the 136000+ Unicode letters -- (The grammar does exist, but takes too long to write out. -- There are notations other than grammars that can capture this.)edcba → "e"* "d"* "c"* "b"* "a"*
same01OrSame12 → same01 "2"* | "0"* same12 same01 → ε | "0" same01 "1" -- this is just (0^n)(1^n) same12 → ε | "1" same12 "2" -- this is just (1^n)(2^n)
noThreeStraightZeros → (atMostTwoZeros "1")* atMostTwoZeros atMostTwoZeros → ε | "0" | "00"
twiceAB → chunk* -- each chunk w/ twice as many a's as b's chunk → "a" twiceAB "a" twiceAB "b" -- one way is a--a--b | "a" twiceAB "b" twiceAB "a" -- another way is a--b--a | "b" twiceAB "a" twiceAB "a" -- third and last way is b--a--aanbnanbn → ("a" 0 "b" "a" 1 "b")? -- Place marks between a's and b's 0 → "a" 0 "b" x -- New a's and b's in the left half x "b" → "b" x -- Move x's to the right of first b's x "a" → "a" x -- Move x's to the right of second a's x 1 → "a" 1 "b" -- When x hits the 1, generate a's and b's at right 0 → ε -- Drop the marks at any time 1 → ε
- Here’s one way do to the grammar (note it is okay for this problem that the grammar be ambiguous, because the question did not specify any precedence or associativity):
Program → FunDecl* Exp FunDecl → id "=" Params "=>" Exp Params → id (",", id)* Exp → numlit | strlit | id | Call | Exp ("+"|"-"|"*"|"/"|"%") Exp | "-" Exp | Exp "!" | Exp "?" Exp ":" Exp | "(" Exp ")" Call → id "(" (Exp ("," Exp)*)? ")" numlit → digit+ ("." digit+)? ("E" ("+" | "-")? digit+)? strlit → "\"" char* "\"" char → "\x0".."\x21" | "\x23".."\x5b" | "\x5d".."\x10fff" | "\\" ("'" | "\"" | "n" | "\\" | "u{" hexes "}") hexes → hexDigit hexDigit? hexDigit? hexDigit? hexDigit? hexDigit? id → (letter | "$") (letter | digit | "_" | "$")* - The tree grammar is:
n: Numlit s: Strlit i: Identifier d: FunDec = i i* e e: Exp = n | s | i | - e | e ! | e + e | e - e | e * e | e / e | e % e | e ? e : e | i e* p: Program = d* e(That’s right, there’s no need to define the lexical grammar in the tree grammar) gcd = (x, y) => y ? gcd(y, x % y) : x cube = (x) => x * x * x "The answer is" + cube(gcd(30, 4!)) + "😦😦"
The drawing program I used did not pick up emojis as text so I used escapes:
-
import x from "x" console.log(93.8 * {x} << x.r[z])
What is the Big Deal?
What this means is that any system of logic powerful enough to make statements about itself has no consistent, complete axiomatization! Once you create a system powerful enough to do self-reference, you cannot have both consistency and completeness.You simply cannot prove all the true statements, unless you have an inconsistent system which proves everything.