The logical error of the Liar Paradox

[Logik]

Although I never saw Curry-Howard before my thinking has always extended way beyond it.

I don't understand what that means? You have always extended beyond an isomorphism?
That's stretching Mathematics/logic somewhat.

I have always thought of these things as a single formalization of the currently set of
all human knowledge.

Yes. You are an idealist.

But the language in which you are formalizing this is not recursively enumerable (e.g computable) and so any equivocation (even in your use of operators like = and ~) blows up triggering the principle of explosion.

Which is why Chomsky's hierarchy is also called a "containment hierarchy". It contains explosions.

This will give you the gist of the idea: https://en.wikipedia.org/wiki/Upper_ontology

Sure. while wearing my phenomenology hat you are talking about perception, mental models.
The map not the territory. Conceptual truth in contrast to facts/measurements.

That's how I use logic. Instrumental to thought, but not an authority on thought.

That is WHY I keep saying that logic is nothing more than LEGO for your mind. It's constructive, not prescriptive.

Human intelligence is not much more than walking this knowledge tree in different ways.
Prolog provides a great base algorithm.

Oh, ok. You've gone onto talking about intelligence now.

Depending on who you ask - that word has many definitions. The peeps in AI research consider "intelligence" as "rational optimization and autonomous goal-setting".

Getting things done in the face of complexity and uncertainty. Robotics etc.

[Logik]

In foundations of mathematics, philosophy of mathematics, and philosophy of logic,
formalism is a theory that holds that statements of mathematics and logic can be
considered to be statements about the consequences of the manipulation of strings.

Yes, BUT mathematicians don't recognize that the digits 1,2,3,4,5.... are strings.

They take the digits and arithmetic for granted.

If we agree that logic is all about symbol manipulation, then you first have to define the rules by which you manipulate 1,2,3,4 etc.

First you have to define your alphabet, but there is a conundrum. A choice exists. Do you go with decimal or duodecimal system?
In what framework do you make such choices? Because your alphabet sure has a consequential effect on your axioms/theorems.

Deductive inference
premise: "five is greater than four"
premise: "four is greater than three"
therefore "five is greater than three"

Formal proof of exactly the same thing
((5 > 4) ∧ (4 > 3)) ⊢ (5 > 3)

Every deduction can be formalized.
Every sound deduction is represented by a formal proof to a theorem consequence.
This might be a little less clear to people unaware of the ways that natural language can be formalized.

Propositional logic provide the overview of this.
The details of converting English into math seem impossible to most.

OK, but deduction is only one of the algorithms of reasoning.
What about abduction?
What about induction?
What about pattern recognition?
What about counterfactual reasoning?

To speak only of deduction necessarily means your system is incomplete. In the sense that it doesn't describe the process of "reasoning" completely.

[PeteOlcott]

Although I never saw Curry-Howard before my thinking has always extended way beyond it.

I don't understand what that means? You have always extended beyond an isomorphism?
That's stretching Mathematics/logic somewhat.

I have always thought of these things as a single formalization of the currently set of
all human knowledge.

I have always extended the isomorphism to include the entire currently existing set of human knowledge.

Yes. You are an idealist.

But the language in which you are formalizing this is not recursively enumerable (e.g computable) and so any equivocation (even in your use of operators like = and ~) blows up triggering the principle of explosion.

Which is why Chomsky's hierarchy is also called a "containment hierarchy". It contains explosions.

The language in which I formalize the entire set of currently existing set of human knowledge is is specified as a directed acyclic graph.
The folloing provides the gist of the idea of this tree of knowledge.

This will give you the gist of the idea: https://en.wikipedia.org/wiki/Upper_ontology

Sure. while wearing my phenomenology hat you are talking about perception, mental models.
The map not the territory. Conceptual truth in contrast to facts/measurements.

That's how I use logic. Instrumental to thought, but not an authority on thought.

That is WHY I keep saying that logic is nothing more than LEGO for your mind. It's constructive, not prescriptive.

Yet when even a tiny subset of the current set of all human knowledge is fully formalized in a language such as Cycorp's CycL this mere logic progresses to becoming an actual human mind.

Human intelligence is not much more than walking this knowledge tree in different ways.
Prolog provides a great base algorithm.

Oh, ok. You've gone onto talking about intelligence now.

Depending on who you ask - that word has many definitions. The peeps in AI research consider "intelligence" as "rational optimization and autonomous goal-setting".

Getting things done in the face of complexity and uncertainty. Robotics etc.

From a strong AI perspective Human Intelligence is nothing more than being able
to duplicate the functional end result of a human mind.

[PeteOlcott]

In foundations of mathematics, philosophy of mathematics, and philosophy of logic,
formalism is a theory that holds that statements of mathematics and logic can be
considered to be statements about the consequences of the manipulation of strings.

Yes, BUT mathematicians don't recognize that the digits 1,2,3,4,5.... are strings.

They take the digits and arithmetic for granted.

If we agree that logic is all about symbol manipulation, then you first have to define the rules by which you manipulate 1,2,3,4 etc.

First you have to define your alphabet, but there is a conundrum. A choice exists. Do you go with decimal or duodecimal system?
In what framework do you make such choices? Because your alphabet sure has a consequential effect on your axioms/theorems.

Deductive inference
premise: "five is greater than four"
premise: "four is greater than three"
therefore "five is greater than three"

Formal proof of exactly the same thing
((5 > 4) ∧ (4 > 3)) ⊢ (5 > 3)

Every deduction can be formalized.
Every sound deduction is represented by a formal proof to a theorem consequence.
This might be a little less clear to people unaware of the ways that natural language can be formalized.

Propositional logic provide the overview of this.
The details of converting English into math seem impossible to most.

OK, but deduction is only one of the algorithms of reasoning.
What about abduction?
What about induction?
What about pattern recognition?
What about counterfactual reasoning?

To speak only of deduction necessarily means your system is incomplete. In the sense that it doesn't describe the process of "reasoning" completely.

Those other things can also be formalized in terms of deduction yet deduction
is the necessary prerequisite that must be done first.

We have to maintain a single-minded focus on formal proofs to theorem
consequences as expressing sound deduction to true conclusions until
we have a consensus. Any distraction away from this crucial point could
make success impossible: ∀F∀x(True(F, x) ↔ (F ⊢ x))

Cycorp has the set of human common sense already encoded it took the 700 labor years.
Deep Learning seem to have pattern recognition down pat yet is mostly useless for natural language.

[wtf]

Truth is simply a relation between facts/axioms and other expressions of language.
This can be specified as a knowledge ontology and processed by languages like Prolog.
A knowledge ontology is a tree of knowledge.

You're painfully unaware of the distinction between provability and truth; respectively syntax and semantics. This error underlies all your other errors.

[Logik]

I have always extended the isomorphism to include the entire currently existing set of human knowledge.

OK. Let A be the set of HumanKnowledge
If B is to be isomorphic to A, then B must contain the same number of elements as A.

How many elements are in A?

Hint: you are straddling the symbolic/numeric fence

The language in which I formalize the entire set of currently existing set of human knowledge is is specified as a directed acyclic graph.
The folloing provides the gist of the idea of this tree of knowledge.

You don't seem to draw a distinction between an acyclic directed graph and a tree? They are different, but you seem to be using the terms interchangeably.

Either way. In both cases you NEED a point of origin. Root. An axiom. Truth.

If A is the set of HumanKnowledge, which is ALSO represented by an acyclic graph (whereas in the previous paragraph you claimed that it's a set)

Then it necessarily follows that:
1. Human Knowledge can be conceptualised as both a set AND a graph. Because different conceptions of the same object are necessarily isomorphic then there exists a mathematical function to convert the set of HumanKnowledge into the graph of HumanKnowledge.

What would you call this transformation function?

2. The directed graph A which represents all human knowledge has an axiom. Point of origin for all deduction. An undeniable truth.

Can you please state this axiom?

Yet when even a tiny subset of the current set of all human knowledge is fully formalized in a language such as Cycorp's CycL this mere logic progresses to becoming an actual human mind.

Yes. We tried Expert Systems in the 80s. They don't work for a number of flawed assumptions (all of which you are committing right now): https://en.wikipedia.org/wiki/Expert_sy ... advantages

Number 1 problem of your model so far being - your system is not dynamic. Has no mechanism for updating the Tree of Knowledge as new information arrives.

Human intelligence is not much more than walking this knowledge tree in different ways.
Prolog provides a great base algorithm.

Human intelligence is much more than that. Human intelligence creates, updates AND walks the tree of knowledge.
It is self-referential

From a strong AI perspective Human Intelligence is nothing more than being able
to duplicate the functional end result of a human mind.

That's the lowest bar possible.

The highest bar possible is a general intelligence which can generate/update knowledge orders of magnitude faster than us.
5000 years of human science in a week.

You keep ignoring time. You keep ignoring the power of fast iteration. You keep ignoring compound interest.

[Logik]

You're painfully unaware of the distinction between provability and truth; respectively syntax and semantics. This error underlies all your other errors.

I think this picture from Gödel, Escher, Bach is worth a thousand words.

Truth is a higher notion than proof.

There are both (deductively) unreachable truths and falsehoods.

godel.jpeg

[PeteOlcott]

Truth is simply a relation between facts/axioms and other expressions of language.
This can be specified as a knowledge ontology and processed by languages like Prolog.
A knowledge ontology is a tree of knowledge.

You're painfully unaware of the distinction between provability and truth; respectively syntax and semantics. This error underlies all your other errors.

It is not at all that I am painfully unaware. It is that I can see how one is expressed in terms of the other.
A formal proof to theorem consequences [is] sound deduction to true conclusions.

[Logik]

It is not at all that I am painfully unaware. It is that I can see how one is expressed in terms of the other.
A formal proof to theorem consequences [is] sound deduction to true conclusions.

But theorems are themselves consequences of the axioms.

What are axioms the consequence of?

[wtf]

It is not at all that I am painfully unaware. It is that I can see how one is expressed in terms of the other.
A formal proof to theorem consequences [is] sound deduction to true conclusions.

No, a formal proof is sound deduction to VALID premises. I know you say you spent 20 years on this but you need to retake logic 101.

Think of it this way. Consider the formal system known as the game of chess. It's finite so it's decidable. Given a position you can say whether or not it's a legal position; that is, whether it can be arrived at by a sequence of legal moves.

But is any of it "true?" What if someone asked if the knight "really moves that way in the real world?" The question's absurd. The answer is no. There's no knight in the real world that "moves that way." It's only a formal rule in a formal game. Within the rules of the game there are legal and illegal positions, legal and illegal moves. But it all only exists within itself. You can't find knights moving funny in the real world. Chess isn't "true" in that sense.

Formal systems are about symbol manipulation. Bit flipping if you like. Not truth.

[Logik]

No, a formal proof is sound deduction to VALID premises. I know you say you spent 20 years on this but you need to retake logic 101.

Think of it this way. Consider the formal system known as the game of chess. It's finite so it's decidable. Given a position you can say whether or not it's a legal position; that is, whether it can be arrived at by a sequence of legal moves.

But is any of it "true?" What if someone asked if the knight "really moves that way in the real world?" The question's absurd. The answer is no. There's no knight in the real world that "moves that way." It's only a formal rule in a formal game. Within the rules of the game there are legal and illegal positions, legal and illegal moves. But it all only exists within itself. You can't find knights moving funny in the real world. Chess isn't "true" in that sense.

Formal systems are about symbol manipulation. Bit flipping if you like. Not truth.

This is spot on. Bar a minor nitpick in the duality of language.

There is the distinction between symbolic and numeric approaches.

They are both symbol manipulations in practice, but they start with different philosophies.

[PeteOlcott]

It is not at all that I am painfully unaware. It is that I can see how one is expressed in terms of the other.
A formal proof to theorem consequences [is] sound deduction to true conclusions.

No, a formal proof is sound deduction to VALID premises. I know you say you spent 20 years on this but you need to retake logic 101.

You have that backwards deduction goes from true premises through valid deduction and end up at a true conclusion.
--- Validity and Soundness https://www.iep.utm.edu/val-snd/
--- 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.

In a formal proofs we have the exact same process yet different terminology.
Formal proofs go from empty premises (leaving only true axioms) through rules-of-inference and end up at theorem consequences.

Think of it this way. Consider the formal system known as the game of chess. It's finite so it's decidable. Given a position you can say whether or not it's a legal position; that is, whether it can be arrived at by a sequence of legal moves.

But is any of it "true?" What if someone asked if the knight "really moves that way in the real world?" The question's absurd. The answer is no. There's no knight in the real world that "moves that way." It's only a formal rule in a formal game. Within the rules of the game there are legal and illegal positions, legal and illegal moves. But it all only exists within itself. You can't find knights moving funny in the real world. Chess isn't "true" in that sense.

Formal systems are about symbol manipulation. Bit flipping if you like. Not truth.

The (Curry 2010) notion of a formal system is about truth:
A theory T is a conceptual class consisting of certain of these elementary statements. The elementary statements which belong to T are called the elementary theorems of T and said to be true. In this way, a theory is a way of designating a subset of E which consists entirely of true statements (Curry, Haskell. 2010 Foundations of Mathematical Logic).

http://mathworld.wolfram.com/Axiom.html
An axiom is a proposition regarded as self-evidently true without proof.

As soon as one realizes that the ultimate ground-of- being of all conceptual truth is
(as Curry describes) "elementary statements which belong to T ... said to be true.
then construing his notion of formal system makes perfect sentence and equally
applies to natural as well as formal language.

The ONLY way that we know that a {dog} is a kind of {animal} is because of
{elementary statements which belong to T ... said to be true} where T is
human knowledge expressed in English.

[Logik]

You have that backwards deduction goes from true premises through valid deduction and end up at a true conclusion
...
The (Curry 2010) notion of a formal system is about truth.

Why do you even need deduction if you already have direct access to a priori (axiomatic) truth?

The ONLY way that we know that a {dog} is a kind of {animal} is because of
{elementary statements which belong to T ... said to be true} where T is
human knowledge expressed in English.

Knowing the names/classifications of things does not constitute knowledge.

[PeteOlcott]

You have that backwards deduction goes from true premises through valid deduction and end up at a true conclusion
...
The (Curry 2010) notion of a formal system is about truth.

Why do you even need deduction if you already have direct access to a priori (axiomatic) truth?

The ONLY way that we know that a {dog} is a kind of {animal} is because of
{elementary statements which belong to T ... said to be true} where T is
human knowledge expressed in English.

Knowing the names/classifications of things does not constitute knowledge.

You just contradicted yourself, for indeed knowing anything at all
does constitute knowledge.

[PeteOlcott]

It is not at all that I am painfully unaware. It is that I can see how one is expressed in terms of the other.
A formal proof to theorem consequences [is] sound deduction to true conclusions.

No, a formal proof is sound deduction to VALID premises. I know you say you spent 20 years on this but you need to retake logic 101.

You are using the terminology incorrectly, there is no such
thing as valid premises:
Validity and Soundness https://www.iep.utm.edu/val-snd/
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.