Philosophy Now Forum

Logik wrote: ↑Thu Mar 28, 2019 8:51 am Here's the fundamental problem: you don't know what an "error" is. let alone a "logical error".
Compilers/interpreters are reasonably good at detecting grammatical, semantic or syntactic errors. But they can't guard against intent.

Any proposition you furnish - I can construct a logical system (with a set of axioms) to assert it true OR false.

If you expect input X to produce "TRUE" - I'll make it say "FALSE"
If you expect input Y to produce "FALSE" - I'll make it say "TRUE"

It's a bit of a nail in that coffin. Garbage in - Garbage out etc...

Any set of rules you produce, I can probably navigate them in a way so that I can control the output of your system.

You can spend another 30000 hours trying to understand it from a book, or you can just go to DEF CON ( https://en.wikipedia.org/wiki/DEF_CON ) and have a 13 year old demonstrate it to you.

Mathematical or logical "proof" is not worth shit in the real world. Only proof-of-work is.

∀x Bachelor(x) → ~Married(x)

PeteOlcott wrote: ↑Thu Mar 28, 2019 6:29 pm ∀x Bachelor(x) → ~Married(x)

1. Negative.

Semantic overload. The word "Bachelor" has an alternative meaning.

a person who holds a first degree from a university or other academic institution (only in titles or set expressions).

2. The meaning which you refer to is "a man who is not and has never been married."
∀x Bachelor(x) → ~Married(x)

This is incomplete.

∀x Divorcees(x) → ~Married(x)
∀x Widows(x) & ∀x Widowers → ~Married(x)
∀x 3YearOlds(x) → ~Married(x)
∀x Chandeliers(x) → ~Married(x)

Logik wrote: ↑Thu Mar 28, 2019 8:51 am
Any proposition you furnish - I can construct a logical system (with a set of axioms) to assert it true OR false.

If you expect input X to produce "TRUE" - I'll make it say "FALSE"
If you expect input Y to produce "FALSE" - I'll make it say "TRUE"

Your last reply simply dodged the question.

I understood the above to indicate that you claimed that you could correctly refute any proposition that I furnish.

Here you go refute this: ∀x Bachelor(x) → ~Married(x)

Try and prove that bachelors are married on the basis of the above axiom.

Logik wrote: ↑Thu Mar 28, 2019 8:02 am

PeteOlcott wrote: ↑Wed Mar 27, 2019 7:58 pm All undecidable decision problems are only undecidable because they are stated incorrectly.

We know this. Any algorithm without exit criteria is non-halting (infinite loops).
Scanning through an infinite set is one such scenario (e.g proving all the integers exist).

And the original Turing machine (with an infinite ticker tape) suffers from the same problem: infinitism

PeteOlcott wrote: ↑Wed Mar 27, 2019 7:58 pm http://liarparadox.org/Peter_Linz_HP(Pages_318-319).pdf

It will take me a while to parse your formalization, but intuitively it seems to me you are doing what I described above.

A non-halting finite state machine (infinite loop).

The Halting Problem and the 1931 Incompleteness Theorem have the exactly same
essence as the Liar Paradox. Much later on I found out that the Tarski Undefinability Theorem
is anchored directly in the actual Liar Paradox as its most fundamental basis.

PeteOlcott wrote: ↑Thu Mar 28, 2019 8:02 pm Here you go refute this: ∀x Bachelor(x) → ~Married(x)

Try and prove that bachelors are married on the basis of the above axiom.

It's not an axiom. It's a proposition. And a badly formulated one at that because you keep straddling the set-theoretic and type-theoretic realms.

You are proposing that the logical expression ∀x Bachelor(x) → ~Married(x) is True for all possible inputs x but you haven't show us the implementation of the the functions Bachelor() or Married(). Worst of all, you have failed to define what "x" is.
You have also failed to define HOW (given any particular x) the function Bachelor(x) DECIDES whether to return true or false.

Lets normalize everything into functional notation.

1. The semantics of "→" are defined as follows:

A → B is true if and only if B can be true and A can be false but not vice versa

If A is true and B is false

So lets define "→" as implication(A,B). The truth-table is as follows:

Let 0 ⇔ False
Let 1 ⇔ True

implication(0,0) ⇔ True
implication(0,1) ⇔ True
implication(1,0) ⇔ False
implication(1,1) ⇔ True

So then....

∀x: implication(Bachelor(x), ~Married(x)) ⇔ True

The way to disprove your proposition then is to find a value of x such that:
Bachelor(x) ⇔ True
Married(x) ⇔ True

Go ahead and show us the definition of the functions Bachelor() and Married(), and the type-definition for "x".

I can tell you right now. I am your black swan.

I have a Bachelors degree. I am also Married.

Logik wrote: ↑Thu Mar 28, 2019 10:25 pm

PeteOlcott wrote: ↑Thu Mar 28, 2019 8:02 pm Here you go refute this: ∀x Bachelor(x) → ~Married(x)

Try and prove that bachelors are married on the basis of the above axiom.

It's not an axiom. It's a proposition. And a badly formulated one at that because you keep straddling the set-theoretic and type-theoretic realms.

Rudolf Carnap provided that axiom in his 1952 paper "Meaning Postulates", which is the first time that I am aware of that anyone ever formalized the semantic meaning of natural language sentences. Richard Montague went on to add very much more to this seminal work.

PeteOlcott wrote: ↑Thu Mar 28, 2019 11:21 pm Rudolf Carnap provided that axiom in his 1952 paper "Meaning Postulates", which is the first time that I am aware of that anyone ever formalized the semantic meaning of natural language sentences. Richard Montague went on to add very much more to this seminal work.

Ok. Your approach/strategy confuses me.

In one thread you say you come from computer science background, you speak of Curry-Howard systems, but then you keep talking about axioms.

I don't think you recognize the fence you are straddling.

Lambda calculus (the generalization of Turing's work) contains NO axioms. https://en.wikipedia.org/wiki/Lambda_calculus
In a computational paradigm, speaking of axioms necessarily lands you in the land of cellular automaton.

Further, you are straddling the formalism <-> natural language fence. I would strongly suggest you leave natural language out of this one until you understand what formal systems are and how formal systems work. They are strictly about thought (computation).

Natural language is about communication NOT computation.

Logik wrote: ↑Fri Mar 29, 2019 7:57 am

PeteOlcott wrote: ↑Thu Mar 28, 2019 11:21 pm Rudolf Carnap provided that axiom in his 1952 paper "Meaning Postulates", which is the first time that I am aware of that anyone ever formalized the semantic meaning of natural language sentences. Richard Montague went on to add very much more to this seminal work.

Ok. Your approach/strategy confuses me.

In one thread you say you come from computer science background, you speak of Curry-Howard systems, but then you keep talking about axioms.

I don't think you recognize the fence you are straddling.

Lambda calculus (the generalization of Turing's work) contains NO axioms. https://en.wikipedia.org/wiki/Lambda_calculus
In a computational paradigm, speaking of axioms necessarily lands you in the land of cellular automaton.

Further, you are straddling the formalism <-> natural language fence. I would strongly suggest you leave natural language out of this one until you understand what formal systems are and how formal systems work. They are strictly about thought (computation).

Natural language is about communication NOT computation.

I don't speak of Curry-Howard systems. I only refer to one quote of Curry indicating that a formal system is constructed on the basis of axioms and these axioms have the semantic value of true.

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 2010).

I also refer to one quote from Braithwaite indicating that formal proofs express deductive inference:
The chain of symbolic manipulations in the calculus corresponds to and represents the chain of deductions in the deductive system. (Braithwaite 1962: 2)

A theorem is a subset of all formal proofs in that it has no false premises, thus has the same starting point as sound deduction.

When we combine these ideas together we get formal systems deriving theorem consequences express sound deductive inference.

The whole purpose behind all of my threads is to correctly formalize the notion of truth ∀x True(x) ↔ ⊢ x and use this formalization to refute Tarski Gödel and the Liar Paradox.

PeteOlcott wrote: ↑Fri Mar 29, 2019 4:36 pm I don't speak of Curry-Howard systems. I only refer to one quote of Curry indicating that a formal system is constructed on the basis of axioms and these axioms have the semantic value of true.

In which case... are you aware that:

1. Logic/Mathematics can only prove things up to an isomorphism and no further?
2. Are you familiar with the Curry-Howard isomorphism and its implications to ligic?

PeteOlcott wrote: ↑Fri Mar 29, 2019 4:36 pm 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 2010).

I also refer to one quote from Braithwaite indicating that formal proofs express deductive inference:
The chain of symbolic manipulations in the calculus corresponds to and represents the chain of deductions in the deductive system. (Braithwaite 1962: 2)

A theorem is a subset of all formal proofs in that it has no false premises, thus has the same starting point as sound deduction.

When we combine these ideas together we get formal systems deriving theorem consequences express sound deductive inference.

The whole purpose behind all of my threads is to correctly formalize the notion of truth ∀x True(x) ↔ ⊢ x and use this formalization to refute Tarski Gödel and the Liar Paradox.

Your theoretical grounding is still in the 50s.

Proofs compute. Algorithms. That's all Mathematics ever was. No Truth there. Sorry.

https://en.wikipedia.org/wiki/Curry%E2% ... espondence

In programming language theory and proof theory, the Curry–Howard correspondence (also known as the Curry–Howard isomorphism or equivalence, or the proofs-as-programs and propositions- or formulae-as-types interpretation) is the direct relationship between computer programs and mathematical proofs.

PeteOlcott wrote: ↑Thu Mar 28, 2019 5:48 am I appreciate your reviews.

Thank you.

PeteOlcott wrote: ↑Thu Mar 28, 2019 5:48 am When we have things such as the Goldbach conjecture things get a little fuzzy.
Whether or not we have currently enough knowledge to decide provability one
way or the other is not the same thing as whether or not provability is possible.

To clarify the above: We distinguish between problems that don't have answers at all in a given formal system; versus problems we just don't happen to know the answer to. For example we KNOW that given the axioms of the system known as ZF, we can neither prove nor disprove the axiom of choice.

We do not know whether there's a proof of Goldbach or its negation; OR whether perhaps it's in the same class as the axiom of choice; independent of the standard axioms.

Also it's worth noting that provability and truth are different things. I gather your viewpoint comes out of regarding them as the same. But provability is purely a syntactic notion. We write down a finite list of symbols, program the symbol manipulation into a computer; and the computer can tell you if a given proof is valid. (Whether it can FIND all proofs on its own is a different question).

Gödel showed that axiomatic systems like that can not entirely capture the notion of mathematical truth. There are always statements that are TRUE yet not PROVABLE.

Gödel was a Platonist, surprisingly. He showed that formal systems can not determine all mathematical truth. And yet Gödel did believe in mathematical truth! He believed there was a truth "out there," and he proved that it is not accessible via the axiomatic method.

I don't know why you think proof is truth. A computer doesn't know truth, it only notices high and low voltages in circuits that we HUMANS choose to interpret as 1's and 0's and then perform all these wonders of modern computing. There is no MEANING in computation. The meaning, and the truth, are supplied by humans.

PeteOlcott wrote: ↑Thu Mar 28, 2019 5:48 am I can commit that to the best of my knowledge and understanding that every
statement of mathematics has either a proof or a disproof but not both.

Ok, fine. You are entitled to make that statement. You have directly contradicted Gödel's first incompleteness theorem. Nobody's found a problem with this theorem for 88 years and some of the smartest people in the world have looked at it. This does not of course mean that you are wrong. Only that the burden is on you to communicate so clearly and so compellingly that people can see you're right. You are falling far short of that expository burden in my opinion.

PeteOlcott wrote: ↑Thu Mar 28, 2019 5:48 am A refutation of the 1931 Incompleteness Theorem would not necessarily directly
have this as its consequence.

Yes of course it would. The claim that there exists a consistent formal axiomatic system that decides every proposition is the direct negation of Gödel's first incompleteness theorem.

PeteOlcott wrote: ↑Thu Mar 28, 2019 5:48 am I would not bet my soul that there is not another
undiscovered Incompleteness proof.

Ah I'm really glad you mentioned it, because when you originally said that incompleteness was "erroneous," you did not disambiguate two meanings of that word:

a) Gödel's result is false. What's true is the direct negation of incompleteness; namely, that there IS a complete, consistent, axiomatic foundation for mathematics that decides every proposition.

b) Gödel's result happens to be true, but his proof was flawed. In this case there is still no complete, consistent, axiomatic foundation for math. But at present we just don't know, because Gödel didn't actually prove it one way or the other.

Can you be more clear therefore about the meaning of "erroneous?" This question came up on my first reading and I'm glad that you see the problem.

PeteOlcott wrote: ↑Thu Mar 28, 2019 5:48 am To the best of my current understanding
any Incompleteness proof is analogous to proving that 3 > 5, categorically impossible.

There already is a beautiful and universally accepted incompleteness proof. And it's been re-done several ways. Turing's Halting proof is not a complete equivalent as I understand it but it's a step towards it. Chaitin has beautiful information-theoretic proofs for all these results. Are you aware of his work?

So yeah you MIGHT be a genius with a brand new paradigm. After all they called Einstein crazy. Less well known is that Newton got quite a bit of contemporary pushback on his ideas of gravity. So there is always the nonzero possibility that you're right and everyone else is wrong.

I'm just not seeing compelling evidence. Nor humility. Do you really think you're right and that everybody else is wrong? Not only in mathematical logic, but in computer science as well? What are the odds?

PeteOlcott wrote: ↑Thu Mar 28, 2019 5:48 am I don't know or care about any other consequences because this is too much
like counting my chickens before they hatch.

To me it says that you haven't thought your own ideas through.

PeteOlcott wrote: ↑Thu Mar 28, 2019 5:48 am I have already addressed this one
key consequence before and you did not notice.

I haven't read much of this thread. I only saw that one paragraph where you claimed to have refuted Gödel, Turing, and Tarski; and I've been challenging you on those claims.

PeteOlcott wrote: ↑Thu Mar 28, 2019 5:48 am It seems like your key consequence is at the root of Hilbert's program:
https://en.wikipedia.org/wiki/Hilbert%2 ... rt's_progr
am
For that reason it makes perfect sense that it would be very important to you.

It's not very important to me at all. Hilbert expressed a hope, the same hope of the logicists like Frege, that mathematical truth could be reduced to symbolic manipulation. Gödel and Turing smashed that hope all to hell and that was a long time ago. The results have been checked and rechecked and we've all accepted them and moved on.

PeteOlcott wrote: ↑Thu Mar 28, 2019 5:48 am Because I come from a computer science background I think of all of these things
from a formalist perspective.

If you are a formalist, why do you think provability is truth? THAT'S THE DIRECT OPPOSITE OF FORMALISM. Jeez man.

PeteOlcott wrote: ↑Thu Mar 28, 2019 5:48 am 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!! You and I agree on that definition. So why are you saying that provability equals truth? Or is that Logic saying that and you're not saying that? Maybe you can straighten me out on that point.

Logik wrote: ↑Fri Mar 29, 2019 4:55 pm

PeteOlcott wrote: ↑Fri Mar 29, 2019 4:36 pm I don't speak of Curry-Howard systems. I only refer to one quote of Curry indicating that a formal system is constructed on the basis of axioms and these axioms have the semantic value of true.

In which case... are you aware that:

1. Logic/Mathematics can only prove things up to an isomorphism and no further?
2. Are you familiar with the Curry-Howard isomorphism and its implications to ligic?

Your theoretical grounding is still in the 50s.
Proofs compute. Algorithms. That's all Mathematics ever was. No Truth there. Sorry.

https://en.wikipedia.org/wiki/Curry%E2% ... espondence

In programming language theory and proof theory, the Curry–Howard correspondence (also known as the Curry–Howard isomorphism or equivalence, or the proofs-as-programs and propositions- or formulae-as-types interpretation) is the direct relationship between computer programs and mathematical proofs.

Although I never saw Curry-Howard before my thinking has always extended way beyond it.
I have always thought of these things as a single formalization of the currently set of
all human knowledge.

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

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

My thinking never has been anchored in the 1950's I had the same ideas as Curry and
Braithwaite already combined into my generic truth predicate before I had even
read what they said.

I only refer to them in retrospect to prove that my own ideas are not nonsense.

wtf wrote: ↑Sat Mar 30, 2019 3:05 am Also it's worth noting that provability and truth are different things. I gather your viewpoint comes out of regarding them as the same. But provability is purely a syntactic notion. We write down a finite list of symbols, program the symbol manipulation into a computer; and the computer can tell you if a given proof is valid. (Whether it can FIND all proofs on its own is a different question).

I am going to break this huge post down and address each key point one at a time.
Formal proofs are merely a way to write down deductive inference as soon as
we have a language such as CycL that can formalize any natural language
statement every detail of any deduction can be specified formally.

wtf wrote: ↑Sat Mar 30, 2019 3:05 am I don't know why you think proof is truth. A computer doesn't know truth, it only notices high and low voltages in circuits that we HUMANS choose to interpret as 1's and 0's and then perform all these wonders of modern computing. There is no MEANING in computation. The meaning, and the truth, are supplied by humans.

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.

wtf wrote: ↑Sat Mar 30, 2019 3:05 am
Ah I'm really glad you mentioned it, because when you originally said that incompleteness was "erroneous," you did not disambiguate two meanings of that word:

a) Gödel's result is false. What's true is the direct negation of incompleteness; namely, that there IS a complete, consistent, axiomatic foundation for mathematics that decides every proposition.

b) Gödel's result happens to be true, but his proof was flawed. In this case there is still no complete, consistent, axiomatic foundation for math. But at present we just don't know, because Gödel didn't actually prove it one way or the other.

Can you be more clear therefore about the meaning of "erroneous?" This question came up on my first reading and I'm glad that you see the problem.

The counter-example that he used for the basis of his conclusion is incorrect thus his basis ceases to be valid:
In other words this sentence is false: ∃F ∈ Formal_Systems (∃G ∈ Language(F) (G ↔ ~(F ⊢ G)))

The first incompleteness theorem states that in any consistent formal system F within which a certain amount of arithmetic can be carried out, there are statements of the language of F which can neither be proved nor disproved in F. (Raatikainen, Panu 2018).

There are no such statements G of the language of F.
G is merely self-contradictory.

wtf wrote: ↑Sat Mar 30, 2019 3:05 am

PeteOlcott wrote: ↑Thu Mar 28, 2019 5:48 am Because I come from a computer science background I think of all of these things
from a formalist perspective.

If you are a formalist, why do you think provability is truth? THAT'S THE DIRECT OPPOSITE OF FORMALISM. Jeez man.

PeteOlcott wrote: ↑Thu Mar 28, 2019 5:48 am 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!! You and I agree on that definition. So why are you saying that provability equals truth? Or is that Logic saying that and you're not saying that? Maybe you can straighten me out on that point.

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.