Refuting Incompleteness and Undefinability

[PeteOlcott]

When an expression is shown to be unprovable by diagonalization this masks
over the key detail that it is only unprovable because it is ill-formed.

∀F ∈ Formal_Systems ∀x ∈ WFF(F) (True(F, x) ↔ (F ⊢ x))

You keep bumping your head against the epistemic problem of criterion.

Clearly that is an algorithm in your head which can determine which expression is "well formed" and which expression is "badly formed".
What is your classification rule?

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

Axioms of Truth
(1) ∀F∀x (True(F, x) ↔ (F ⊢ x))
(2) ∀F∀x (False(F, x) ↔ (F ⊢ ~x))
(3) ∀F∀x (~True(F, x) ↔ ~(F ⊢ x))

G ↔ ~(F ⊢ G) Means that G has the same Truth value as its own unprovability in F.
When the RHS ~(F ⊢ G) is true, by Truth axiom(3) we know that x is not true in F.
This contradicts the LHS being true, making the above expression false.

[Logik]

Axioms of Truth
(1) ∀F∀x (True(F, x) ↔ (F ⊢ x))
(2) ∀F∀x (False(F, x) ↔ (F ⊢ ~x))
(3) ∀F∀x (~True(F, x) ↔ ~(F ⊢ x))

G ↔ ~(F ⊢ G) Means that G has the same Truth value as its own unprovability in F.
When the RHS ~(F ⊢ G) is true, by Truth axiom(3) we know that x is not true in F.
This contradicts the LHS being true, making the above expression false.

Those are axioms of isomorphism. Not truth.

[PeteOlcott]

Axioms of Truth
(1) ∀F∀x (True(F, x) ↔ (F ⊢ x))
(2) ∀F∀x (False(F, x) ↔ (F ⊢ ~x))
(3) ∀F∀x (~True(F, x) ↔ ~(F ⊢ x))

G ↔ ~(F ⊢ G) Means that G has the same Truth value as its own unprovability in F.
When the RHS ~(F ⊢ G) is true, by Truth axiom(3) we know that x is not true in F.
This contradicts the LHS being true, making the above expression false.

Those are axioms of isomorphism. Not truth.

The prove Tarski is wrong, whatever they are that are what
Tarski "proved" to be impossible.

[Logik]

The prove Tarski is wrong, whatever they are that are what
Tarski "proved" to be impossible.

Tell me what "proof" would convince you and I will construct you an algorithm that evaluates to that value.
I am literally asking you to help me define your own black swan. Help me help you prove yourself wrong.

The fundamental problem with your approach is that you pre-suppose deductive reasoning as the norm for humans. This may well be and a lot of people choose it dogmatically but this universe deduction doesn't produce "100% certain knowledge". There is no such thing.


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

Inductive reasoning is inherently uncertain. It only deals in the extent to which, given the premises, the conclusion is credible according to some theory of evidence. Examples include a many-valued logic, Dempster–Shafer theory, or probability theory with rules for inference such as Bayes' rule. Unlike deductive reasoning, it does not rely on universals holding over a closed domain of discourse to draw conclusions, so it can be applicable even in cases of epistemic uncertainty (technical issues with this may arise however; for example, the second axiom of probability is a closed-world assumption).[5]

Another crucial difference between these two types of argument is that deductive certainty is impossible in non-axiomatic systems such as reality, leaving inductive reasoning as the primary route to (probabilistic) knowledge of such systems.

[PeteOlcott]

Another crucial difference between these two types of argument is that deductive certainty is impossible in non-axiomatic systems such as reality, leaving inductive reasoning as the primary route to (probabilistic) knowledge of such systems.

[/quote]

So in other words the sum of 2 + 3, is only a matter of opinion and thus impossible
to definitely determine.

This is the mindset that has been a pet peeve of mine since I was a teenager,
it allows corrupt politicians to wreak havoc on society.

For years I referred to this as absolute truth and was rejected with religious conviction.
Now I refer to this as axiomatic truth** and correct refutation becomes impossible.

**Axiomatic Truth
Logically following from axioms which are expressions of language
(such as: "dogs are animals") that are defined to be true.

[Logik]

So in other words the sum of 2 + 3, is only a matter of opinion and thus impossible
to definitely determine.

Depends if you are using numeric or symbolic methods.

This is the mindset that has been a pet peeve of mine since I was a teenager,
it allows corrupt politicians to wreak havoc on society.

Your mindset is more harmful. It leads to dogma.

For years I referred to this as absolute truth and was rejected with religious conviction.
Now I refer to this as axiomatic truth** and correct refutation becomes impossible.

**Axiomatic Truth
Logically following from axioms which are expressions of language
(such as: "dogs are animals") that are defined to be true.

Religious truth. Axiomatic truth. It's all foudnationalism ( https://en.wikipedia.org/wiki/Foundationalism ).
It's all dogma.

[PeteOlcott]

So in other words the sum of 2 + 3, is only a matter of opinion and thus impossible
to definitely determine.

Depends if you are using numeric or symbolic methods.

Unless expressly superseded by overloaded meanings conventional symbols retain their conventional meaning.

In an knowledge ontology the above symbols would each be defined by a single algorithmic semantic meaning.

[Logik]

Unless expressly superseded by overloaded meanings conventional symbols retain their conventional meaning.

Conventional in what sense? The USA uses the Imperial system. Europe uses the metric system.
Computer scientists use binary, octal and hexadecimal number systems frequently.
Specialists in just about every field use non-conventional jargon.

Sounds to me like you have some idealised idea of how language ought to be used which greatly diverges from how language is actually used.

Language/logic is instrumental, not prescriptive. I use it however works for me.

In an knowledge ontology the above symbols would each be defined by a single algorithmic semantic meaning.

Have you ever heard of the principle of Equifinality?

For any input-output behavior there are an infinite number of equal-value functions.

f(a,b) = a + b = 5 = 2 + 3
g(c,d) = c - d + 1 = 5 = 7 - 3 + 1
h(x,y) = c + d - 45 = 5 = 49 + 51 - 45

[PeteOlcott]

Unless expressly superseded by overloaded meanings conventional symbols retain their conventional meaning.

Conventional in what sense? The USA uses the Imperial system. Europe uses the metric system.
Computer scientists use binary, octal and hexadecimal number systems frequently.
Specialists in just about every field use non-conventional jargon.

There is no metric system of integers. And when decimal digits are specified and not defined to be some other number system then decimal is implicitly specified. Whenever type do need to be specified Minimal Type Theory specifies them.

https://www.researchgate.net/publicatio ... y_YACC_BNF

[PeteOlcott]

Sounds to me like you have some idealised idea of how language ought to be used which greatly diverges from how language is actually used.

It is merely slightly augmented first order predicate logic.
https://www.researchgate.net/publicatio ... y_YACC_BNF

Unlike FOL MTT specifies any logic order from 0 to N and it does so with optional types.
I changed it and made the types optional so that FOL would be a subset.

[Logik]

There is no metric system of integers.

There's an alphabet of digits for every number system.

Binary: 0,1
Ternary: 0,1,2
Octal, 0,1,2,3,4,5,6,7
Decimal 0,1,2,3,4,5,6,7,8,9,
Hexadecimal, 0,1,2,3,4,5,6,7,8,9,A,B,C,D,E,F

And when decimal digits are specified and not defined to be some other number system then decimal is implicitly specified.

According to which authority?

Whenever type do need to be specified Minimal Type Theory specifies them.

As recently as one hour ago you claimed that anybody who is not explicit in their meaning is a liar.

I insist that you adhere to the principles of strongly typed programming languages and explicitly declare ALL of your types.

[Logik]

I changed it and made the types optional so that FOL would be a subset.

In accordance with your own standards I insist that you be explicit. Everywhere and always. In order to avoid "lying".

Therefore I insist on strong and static typing. https://en.wikipedia.org/wiki/Strong_an ... e-checking

As per:

My system would use GUIDs** so that there is only one unique integer per semantic meaning.

[Scott Mayers]

@PeteOlcott,

Why are you using distinct threads to argue the same point? Are you attempting to measure the same value of your theory/theorem as true if one of the threads gets a pass regardless of some counter-proof elsewhere?

[not implying a necessary insult,...just wondering why the separate threads are required in your opinion.]

[PeteOlcott]

I changed it and made the types optional so that FOL would be a subset.

In accordance with your own standards I insist that you be explicit. Everywhere and always. In order to avoid "lying".

Therefore I insist on strong and static typing. https://en.wikipedia.org/wiki/Strong_an ... e-checking

As per:

My system would use GUIDs** so that there is only one unique integer per semantic meaning.

I can easily assign types to variables, assigning them to numeric digits would not be required
because they are already defined by a regular expression of the lexical analyzer.

[Logik]

I can easily assign types to variables, assigning them to numeric digits would not be required
because they are already defined by a regular expression of the lexical analyzer.

Why do you take the digits for granted?

The string "1" is not as the digit 1.
The integer 1 is not the same thing as the real number 1.0

I insist that you define everything. From first principles. In Lambda calculus.

Alphabet.
Digits.
Arithmetic.
Operators.
Type-conversions.
Error handling.

The lot! I want strong and strict typing.