[bitL]

Isn't Gödel's incompleteness a consequence of overly ambitious material implication properties? When you look at the truth table:

A | B | A -> B

0 | 0 | 1

0 | 1 | 1

1 | 0 | 0

1 | 1 | 1

I fail to see why all except for 1 -> 0 = 0 aren't undefined. I understand reasoning behind why this was done, but mixing unrelated predicates seems like a generally bad idea, even if it allows mechanical proofs.

Aren't there already "complete" systems like relevance logic? Now with computers we can perhaps make proofs we need "relevant" instead of being based on fundamentally incomplete though "simpler" logic?

[contravariant]

Logic already has separate symbols for 'A implies B' and 'A proves B', where the first can be considered equivalent to '(not A) or B' for all intents and purposes. Since 'A proves B' seems like the very definition of relevance, the only part you could possibly object to is that 'A proves B' implies 'A implies B', but that's given since the alternative would lead to a contradiction where A proves B, but B is false while A is not.

Also, if I understand you correctly you're trying to 'fix' incompleteness by making A -> B undecidable, which seems like it would achieve the opposite.

[cvoss]

The first incompleteness theorem shows that, in a sense, the culprit of a logic's incompleteness is not its "simplicity" but its "complexity": if the logic is rich enough to include Peano arithmetic, then it is incomplete. Compared to mathematics in general, a complete logic system is far less powerful and cannot be used to prove nearly as many interesting things.

[burntrelish1273]

Undefined / don't care states also allow for simpler physical implementations. For those whom did EE/CS undergrad might remember Karnaugh maps.

[vilhelm_s]

Well no, Gödel's incompleteness theorem doesn't really have anything to do with material implication. It tells us that there is some formula G such that neither G nor ¬G is provable. Proof systems for relevance logic restrict valid derivations compared to classical propositional logic (relevance logic requires you to use the antecedent), so they can prove even fewer things.

[acchow]

  1 -> 0 = 0

What does this mean? Is the 0 after the equals the antecedent? Consequent?

[pmcjones]

(1 -> 0) = 0.

In other words, (true implies false) is false.

[acchow]

"is false" doesn't mean anything in Godel's system. That's too high level and imprecise. We're dealing with only symbol manipulation here. We only have provability (which really is "there exists a derivation for") - we don't have "truth".