Eliminating Undecidability and Incompleteness in Formal Systems (As simple as possible)

[Logik]

No you are wrong. We do not require a whole new formal system every time
that we add an axiom. We only need this when axioms form contradictions.

This is where you and I differ fundamentally.

When you hit a contradiction you invent a new formal system. Because you are optimising for consistency.
I am optimising for power. Power in the same sense as it is used in the statement "any recursive system that is sufficiently powerful, cannot be both consistent and syntactically complete."

Paraconsistency works for me in English. And it works for me in meta-languages.

A paraconsistent logic is a logical system that attempts to deal with contradictions in a discriminating way.

[PeteOlcott]

Every axiom must have an associated finite string. It cannot simply sit inside someone's head.

Sure. But the meaning of strings is different from system to system.

2+2 = 4 (decimal)
2+2 = 11 (ternary)

IF "=" means "semantic equivalence"

∴ 4 = 11

IF "=" means "symbolic equivalence" then it's false.

I am (as Rudolf Carnap did) providing semantic specification syntactically, so I can't tell what you are doing.
10 + 10 = 100 in binary. 10 + 10 = 20 when binary is not specified.

[PeteOlcott]

No you are wrong. We do not require a whole new formal system every time
that we add an axiom. We only need this when axioms form contradictions.

This is where you and I differ fundamentally.

When you hit a contradiction you invent a new formal system. Because you are optimising for consistency.
I am optimising for power. Power in the same sense as it is used in the statement "any recursive system that is sufficiently powerful, cannot be both consistent and syntactically complete."

Paraconsistency works for me in English. And it works for me in meta-languages.

A paraconsistent logic is a logical system that attempts to deal with contradictions in a discriminating way.

That seems a little nutty, you are aiming for inconsistency.
Instead I aim for completeness and consistency, and the sound
deductive inference model provides this because it decides:

Provable(X) is the same thing as True(X)
Refutable(X) is the same thing as False(X)
Otherwise Unsound(X) (screwed up no good X).

[Logik]

That seems a little nutty, you are aiming for inconsistency.

That seems like a strawman.

My aim is to minimize inconsistencies. Your aim is to eliminate them because you have no viable strategies for containing the principle of explosion.

I do. Para-consistency.

Consistent logics are all-or-nothing systems. Far too fragile to be useful in the real world. Antifragility is better.

It's the difference between idealism and pragmatism. All models are wrong - some are useful.

Instead I aim for completeness and consistency

That is why you keep ending up with truisms/trivialities. You are (quite literally) discarding the consequences of Godel incompleteness.

Consistency and completeness comes at the cost of utility. Power.

[Speakpigeon]

Yeah, good strategy, I think it should work. If you're unable to understand logic, try to understand something else and call it "logic".
EB

[PeteOlcott]

My aim is to minimize inconsistencies. Your aim is to eliminate them because you have no viable strategies for containing the principle of explosion.

Perhaps you never heard of the sound deductive inference model (SDIM) before?

https://www.iep.utm.edu/val-snd/
Validity and Soundness
A deductive argument is said to be valid if and only if it takes a form that makes it impossible for the premises to be true and the conclusion nevertheless to be false. Otherwise, a deductive argument is said to be invalid.

A deductive argument is sound if and only if it is both valid, and all of its premises are actually true. Otherwise, a deductive argument is unsound.

https://en.wikipedia.org/wiki/Principle_of_explosion

X ∧ ¬X → Y is valid according to POE yet unsound because of SDIM.

[PeteOlcott]

Yeah, good strategy, I think it should work. If you're unable to understand logic, try to understand something else and call it "logic".
EB

When we convert the formal proofs to theorem consequences of symbolic logic
(something you may not understand) to the sound deductive inference model
(something you may understand) we get this end result:

Summing it up:
True(X) is Provable(X) from True Premises.
False(X) is Provable(¬X) from True Premises.
Otherwise Unsound(X).

Which eliminates incompleteness and inconsistency from formal systems.

[Logik]

Perhaps you never heard of the sound deductive inference model (SDIM) before?

ALL MODELS ARE WRONG

A deductive argument is said to be valid if and only if it takes a form that makes it impossible for the premises to be true and the conclusion nevertheless to be false. Otherwise, a deductive argument is said to be invalid.

Read this carefully. Very. Very. Carefully.
Compute the consequences of this statement.
Also compute the consequences of its negation and its contra-positive.

Then consider: Is an argument valid when the premises are SAID to be true (axiomatically) yet there is non-zero (1 in 10^10000000000000 probability) that the conclusion is false. Is the POSSIBILITY of a counter-example sufficient to render the argument invalid?

Axiom: All swans are white.
Conclusion based on SDIM: If it is a swan then it is white.
Conclusion based on SDIM: If it is black then it is not a swan.
Empirical observation: A black swan.

Do you understand that:

1. The "validity" criterion is INCREDIBLY strict and mandates absolute truths (e.g axioms).
2. The "validity" criterion is incompatible with the scientific principle of falsification.

Your model of truth pre-supposes completeness of knowledge. Because for as long as your knowledge is incomplete - your axiom can always be contradicted by new information.

Human knowledge is incomplete. Fact.
So how can any argument be valid if there is a non-zero probability of the conclusion being false?

[Speakpigeon]

Let's try code to teach lessons... As if that could help!

LOGIC CLASS
Start
:Lesson One:
A → B ⊢ ¬(A ∧ ¬B)
:Lesson Two:
A ∧ (A → B) ⊢ B
:Lesson Three:
¬B ∧ (A → B) ⊢ ¬A
:Lesson Four:
A ∧ ¬B ⊢ ¬(A → B)
Print "That's all you need to know!"
Print "Where's the problem already?"
End

EB

[Speakpigeon]

Human knowledge is incomplete. Fact.
So how can any argument be valid if there is a non-zero probability of the conclusion being false?

Because it's a logical argument and the validity of a logical argument in assessed independently of the truth of the premises.
Aristotle understood that, the Stoics understood that, the Scholastics understood that, all logical pundits throughout the world understand that...
Only ignoramuses and idiots don't understand that, and also our own in-house self-professed computer scientist. Quirky?
EB

[Logik]

Because it's a logical argument and the validity of a logical argument in assessed independently of the truth of the premises.

This keeps going over your head, eh? My grudge with "logical validity" is not about the truth of the premises.
It's about the IMPOSSIBILITY of falsity of the conclusions.

Deductive validity is in direct conflict with empirical falsification.

Aristotle understood that, the Stoics understood that, the Scholastics understood that, all logical pundits throughout the world understand that...
Only ignoramuses and idiots don't understand that, and also our own in-house self-professed computer scientist. Quirky?

Then by your standards I am an ignoramus and an idiot. Lucky me!

There are much worse things you could've called me. Such as an Aristotelian, a Stoic, a Scholastic. Or worse yet - you could've called me a philosopher.

None of your role models possessed anything that would qualify as "understanding" or "knowledge" in my world.

[Logik]

Let's try code to teach lessons... As if that could help!

LOGIC CLASS
Start
:Lesson One:
A → B ⊢ ¬(A ∧ ¬B)
:Lesson Two:
A ∧ (A → B) ⊢ B
:Lesson Three:
¬B ∧ (A → B) ⊢ ¬A
:Lesson Four:
A ∧ ¬B ⊢ ¬(A → B)
Print "That's all you need to know!"
Print "Where's the problem already?"
End

EB

You can't teach what you don't understand...

Lets start with some questions. Given the Chomsky hierarchy would you say your formalism above is a Type 0, 1, 2 or 3 grammar?

[Speakpigeon]

Let's try code to teach lessons... As if that could help!

LOGIC CLASS
Start
:Lesson One:
A → B ⊢ ¬(A ∧ ¬B)
:Lesson Two:
A ∧ (A → B) ⊢ B
:Lesson Three:
¬B ∧ (A → B) ⊢ ¬A
:Lesson Four:
A ∧ ¬B ⊢ ¬(A → B)
Print "That's all you need to know!"
Print "Where's the problem already?"
End

EB

You can't teach what you don't understand...
Lets start with some questions. Given the Chomsky hierarchy would you say your formalism above is a Type 0, 1, 2 or 3 grammar?

Hello?! We're talking about logic here. You know? Logic? Nah. You don't.
EB

[Logik]

Hello?! We're talking about logic here. You know? Logic? Nah. You don't.
EB

Yes. Precisely logic.

https://en.wikipedia.org/wiki/Logic

The systematic study of the form of valid inference.

https://en.wikipedia.org/wiki/Logical_form

In philosophy and mathematics, a logical form of a syntactic expression is a precisely-specified semantic version of that expression in a formal system.

https://en.wikipedia.org/wiki/Formal_system

A formal system is used to infer theorems from axioms according to a set of rules.

https://en.wikipedia.org/wiki/Formal_language

In mathematics, computer science, and linguistics, a formal language consists of words whose letters are taken from an alphabet and are well-formed according to a specific set of rules.

Now answer my question. Is your formal system a Type 0, 1,2 or 3 in the Chomsky hierarchy.

The answer is trivial for somebody who "knows logic". Roll a dice if you don't know - 25% chance of guessing right!

[Logik]

Hello?! We're talking about logic here. You know? Logic? Nah. You don't.

But the most important question is: What do YOU mean by 'logic'?

https://en.wikipedia.org/wiki/Logic

There is no universal agreement as to the exact scope and subject matter of logic

So many different conceptions

• The tool for distinguishing between the true and the false (Averroes)

• The science of reasoning, teaching the way of investigating unknown truth in connection with a thesis (Robert Kilwardby).

• The art whose function is to direct the reason lest it err in the manner of inferring or knowing (John Poinsot).

• The art of conducting reason well in knowing things (Antoine Arnauld).

• The right use of reason in the inquiry after truth (Isaac Watts).

• The Science, as well as the Art, of reasoning (Richard Whately).

• The science of the operations of the understanding which are subservient to the estimation of evidence (John Stuart Mill).

• The science of the laws of discursive thought (James McCosh).

• The science of the most general laws of truth (Gottlob Frege)