Page 1 of 3

### Converting formal proofs to conform to sound deduction

Posted: Tue Apr 30, 2019 4:03 pm
This post requires some knowledge of the terminology of formal proofs of symbolic logic.

In the same way that not all finite strings are well-formed
formula (when semantic criteria is applied) not all closed
WFF are logic sentences.

Any expression of language that is neither true nor false is
not a logic sentence of any formal system that has been
adapted to conform to the sound deductive inference model.

Logic sentences are always derived from sound deduction. In
the sound deductive inference model this means that there is:
[a connected sequence of valid deductions from true premises to a true conclusion].

When axioms are construed as expressions of language having the
semantic property of Boolean true then the theorem consequences
of formal proofs form:
[a connected sequence of inference from axioms to a true consequence].

In neither case is undecidability, incompleteness or inconsistency possible.

### Re: Converting formal proofs to conform to sound deduction

Posted: Tue Apr 30, 2019 5:01 pm
PeteOlcott wrote: Tue Apr 30, 2019 4:03 pm This post requires some knowledge of the terminology of formal proofs of symbolic logic.

In the same way that not all finite strings are well-formed
formula (when semantic criteria is applied) not all closed
WFF are logic sentences.

Any expression of language that is neither true nor false is
not a logic sentence of any formal system that has been
adapted to conform to the sound deductive inference model.

Logic sentences are always derived from sound deduction. In
the sound deductive inference model this means that there is:
[a connected sequence of valid deductions from true premises to a true conclusion].

When axioms are construed as expressions of language having the
semantic property of Boolean true then the theorem consequences
of formal proofs form:
[a connected sequence of inference from axioms to a true consequence].

In neither case is undecidability, incompleteness or inconsistency possible.
You have successfully managed to hide the ball from yourself again.

All the decision (COMPUTATIONAL!) complexity of your system now hides is in your WFF() function.

The algorithm which decides whether a particular finite string, word, sentence or expression is 'well formed'.

IF you (somehow) succeed in doing this in Prolog then you will rob Prolog of its Turing-completeness.

### Re: Converting formal proofs to conform to sound deduction

Posted: Tue Apr 30, 2019 5:45 pm
Logik wrote: Tue Apr 30, 2019 5:01 pm
PeteOlcott wrote: Tue Apr 30, 2019 4:03 pm This post requires some knowledge of the terminology of formal proofs of symbolic logic.

In the same way that not all finite strings are well-formed
formula (when semantic criteria is applied) not all closed
WFF are logic sentences.

Any expression of language that is neither true nor false is
not a logic sentence of any formal system that has been
adapted to conform to the sound deductive inference model.

Logic sentences are always derived from sound deduction. In
the sound deductive inference model this means that there is:
[a connected sequence of valid deductions from true premises to a true conclusion].

When axioms are construed as expressions of language having the
semantic property of Boolean true then the theorem consequences
of formal proofs form:
[a connected sequence of inference from axioms to a true consequence].

In neither case is undecidability, incompleteness or inconsistency possible.
You have successfully managed to hide the ball from yourself again.

All the decision (COMPUTATIONAL!) complexity of your system now hides is in your WFF() function.

The algorithm which decides whether a particular finite string, word, sentence or expression is 'well formed'.

IF you (somehow) succeed in doing this in Prolog then you will rob Prolog of its Turing-completeness.
https://www.researchgate.net/publicatio ... y_YACC_BNF
As I have already said many times, the above YACC BNF specifies every relevant detail of
this algorithm such that a fully operational parser of every WFF of the MTT language was
automatically generated from this YACC BNF syntax.

It generates an XML parse tree of every WFF MTT expression and rejects all others as not WFF.

MTT is a universal Tarski meta-language that can represent the semantics of any expression
of any formal system, including its own semantics as a directed acyclic graph (DAG).
This DAG is processed in a way comparable to the way that Prolog processes its queries.
Unlike Prolog the MTT DAG can directly represent the connections between every level
of logic from zero to N.

### Re: Converting formal proofs to conform to sound deduction

Posted: Tue Apr 30, 2019 5:49 pm
PeteOlcott wrote: Tue Apr 30, 2019 5:45 pm MTT is a universal Tarski meta-language that can represent the semantics of any expression
of any formal system, including its own semantics as a directed acyclic graph (DAG).
So the MTT language is NOT Turing complete? How do you do shortest-path traversal of the DAG?

And if MTT IS Turing-complete, how are you going to stop me from bootstrapping a Python interpreter in MTT and then doing the exact same shenanigans you keep telling me that I am not "allowed" to do?

### Re: Converting formal proofs to conform to sound deduction

Posted: Tue Apr 30, 2019 6:48 pm
Logik wrote: Tue Apr 30, 2019 5:49 pm
PeteOlcott wrote: Tue Apr 30, 2019 5:45 pm MTT is a universal Tarski meta-language that can represent the semantics of any expression
of any formal system, including its own semantics as a directed acyclic graph (DAG).
So the MTT language is NOT Turing complete? How do you do shortest-path traversal of the DAG?

And if MTT IS Turing-complete, how are you going to stop me from bootstrapping a Python interpreter in MTT and then doing the exact same shenanigans you keep telling me that I am not "allowed" to do?
MTT has an isomorphism to lambda calculus.
MTT is consistent and complete and will not allow introducing any axioms conflicting with its current axioms.

### Re: Converting formal proofs to conform to sound deduction

Posted: Tue Apr 30, 2019 7:36 pm
PeteOlcott wrote: Tue Apr 30, 2019 6:48 pm MTT has an isomorphism to lambda calculus.
PeteOlcott wrote: Tue Apr 30, 2019 6:48 pm MTT is consistent and complete and will not allow introducing any axioms conflicting with its current axioms.
These two claims are incompatible with each other.

If MTT is Turing complete then any and all notions of "formal proof" are isomorphic to algorithms as per Curry-Howard isomorphism

If MTT is Turing complete I can bootstrap myself from MTT into ANY Type 0 Chomsky grammar.

Consistent. Paraconsistent. Dialethic. Quantum.

And then I am back to my old shenanigans where 1 = 0, true = false. Or anything else I want.

It's not so much that MTT "will not allow introducing any axioms conflicting with its current axioms". It's more like "MTT cannot prevent anyone from introducing conflicting axioms".

If I control the input to a Turing-complete system, I control the system. I can make it sing the Star Spangled banner if I want to.

### Re: Converting formal proofs to conform to sound deduction

Posted: Tue Apr 30, 2019 8:11 pm
Logik wrote: Tue Apr 30, 2019 7:36 pm
PeteOlcott wrote: Tue Apr 30, 2019 6:48 pm MTT has an isomorphism to lambda calculus.
PeteOlcott wrote: Tue Apr 30, 2019 6:48 pm MTT is consistent and complete and will not allow introducing any axioms conflicting with its current axioms.
These two claims are incompatible with each other.
MTT the formal language will let you do anything that lambda calculus will allow.

MTT the formal system will know when you are lying to it because it is already populated with axioms.

### Re: Converting formal proofs to conform to sound deduction

Posted: Tue Apr 30, 2019 8:17 pm
PeteOlcott wrote: Tue Apr 30, 2019 8:11 pm MTT the formal system will know when you are lying to it because it is already populated with axioms.

WHICH axioms are you going to populate it with?!?

### Re: Converting formal proofs to conform to sound deduction

Posted: Tue Apr 30, 2019 8:36 pm
Logik wrote: Tue Apr 30, 2019 8:17 pm
PeteOlcott wrote: Tue Apr 30, 2019 8:11 pm MTT the formal system will know when you are lying to it because it is already populated with axioms.

WHICH axioms are you going to populate it with?!?
This system is already populated with the complete set of human common sense:
https://en.wikipedia.org/wiki/Cyc

If we hypothesize that the MTT system is populated with the complete set of
general human knowledge, then trying to tell it that 1 = 0, will be easily refutable
on the basis of its axioms.

### Re: Converting formal proofs to conform to sound deduction

Posted: Tue Apr 30, 2019 8:47 pm
PeteOlcott wrote: Tue Apr 30, 2019 8:36 pm This system is already populated with the complete set of human common sense:
https://en.wikipedia.org/wiki/Cyc
I call bullshit that you can fit all knowledge from the Internet into one consistent system, but lets go with that for 2 seconds.
I'll even pretend that you have (somehow) figured out how to unify incompatible theories like General Relativity and Quantum Mechanics.
PeteOlcott wrote: Tue Apr 30, 2019 8:36 pm If we hypothesize that the MTT system is populated with the complete set of
general human knowledge, then trying to tell it that 1 = 0, will be easily refutable
on the basis of its axioms.
wtf already showed you a mathematical framework in which 1 = 0 is a perfectly valid expression.

So I ask again. WHO chose the axioms and why? Because their "common sense" clearly disagrees with my "common sense".

### Re: Converting formal proofs to conform to sound deduction

Posted: Tue Apr 30, 2019 8:51 pm
Logik wrote: Tue Apr 30, 2019 8:47 pm
PeteOlcott wrote: Tue Apr 30, 2019 8:36 pm This system is already populated with the complete set of human common sense:
https://en.wikipedia.org/wiki/Cyc
I call bullshit that you can fit all knowledge from the Internet into one consistent system, but lets go with that for 2 seconds.
I'll even pretend that you have (somehow) figured out how to unify incompatible theories like General Relativity and Quantum Mechanics.
PeteOlcott wrote: Tue Apr 30, 2019 8:36 pm If we hypothesize that the MTT system is populated with the complete set of
general human knowledge, then trying to tell it that 1 = 0, will be easily refutable
on the basis of its axioms.
wtf already showed you a mathematical framework in which 1 = 0 is a perfectly valid expression.

So I ask again. WHO chose the axioms and why? Because their "common sense" clearly disagrees with my "common sense".
This is also perfectly valid, it is, however, unsound:
Unsound deductive inference (false premise)
(a) All dogs are office buildings
(b) All office buildings have windows
(c) Therefore all dogs have windows

If you want to have the psychotic break from reality and believe that dogs really
are office buildings feel free.

### Re: Converting formal proofs to conform to sound deduction

Posted: Tue Apr 30, 2019 8:55 pm
PeteOlcott wrote: Tue Apr 30, 2019 8:51 pm This is also perfectly valid, it is, however, unsound:
Unsound deductive inference (false premise)
(a) All dogs are office buildings
(b) All office buildings have windows
(c) Therefore all dogs have windows
It's an Idiotic example because you have absolutely no way of introducing modal logic into your ontology.

Lets start from 1st principles, because in 21 years you haven't gotten past 1st grade.

You cannot do deduction in this universe. Because of this:

Logical validity mandates that it is IMPOSSIBLE for the premises to be true yet for the conclusions to be false. This means that ANY Probability (p > 0) that your conclusion is false when the premises are true, a SINGLE counter-example to your deductive rule renders your deduction invalid.

You have no absolute truths in this universe.. You have no real-world objects/phenomena/things for which you can universally say ALL X are Y.

To say ALL X are Y is to say "there is an isomorphism between X and Y". And that only works in formal systems.

### Re: Converting formal proofs to conform to sound deduction

Posted: Tue Apr 30, 2019 11:03 pm
Logik wrote: Tue Apr 30, 2019 8:55 pm To say ALL X are Y is to say "there is an isomorphism between X and Y". And that only works in formal systems.
Really? So when I say "All cats are mammals" that's the same as saying cats are isomorphic to mammals?

This isn't just wrong on the facts, it's meta-wrong. It's a category error.

It's not just that the class of cats is a proper subclass of the class of mammals, so that there are mammals that aren't cats. That's one error but a trivial one.

The deeper error is that you misunderstand the type of objects that isomorphism applies to. When I say that the Cartesian product of the integers mod 3 and the integers mod 2 is the integers mod 6, I'm not asserting a subset relation of any kind. These are two set-theoretic objects that are not the same set at all. But there's a structure-preserving bijection between them. That's got nothing to do with cats and mammals. It's got nothing to do with class or subclass relationships. It's about seemingly DIFFERENT objects that, upon examination, turn out to have the same "structure" in some formal sense.

Let me repeat this to emphasize my point. Isomorphism is about finding two completely different things, then doing a little abstract thought about them, and coming to realize that they are actually the SAME thing -- but ONLY when you restrict your attention to one particular ASPECT of them.

Whereas subclass relations -- all cats are mammals -- is something entirely different. It's about categorical categorization of the class of all things. Aristotelian categories.

I'll add that I haven't been following the thread, but just jumped on this obvious mistake. Bad habit of mine. So if I'm being too picky just let me know. But cats and mammals have nothing to do with isomorphism.

### Re: Converting formal proofs to conform to sound deduction

Posted: Tue Apr 30, 2019 11:23 pm
wtf wrote: Tue Apr 30, 2019 11:03 pm Really? So when I say "All cats are mammals" that's the same as saying cats are isomorphic to mammals?
OK. so you are using "are" to mean "subset of". Cool. We can play that game up and down the layers of abstraction right until we get to the set of all sets.

And then I am going to ask you....
wtf wrote: Tue Apr 30, 2019 11:03 pm This isn't just wrong on the facts, it's meta-wrong. It's a category error.
...how did you classify your first subset. What is your first category and what's your classification function?

All categories are errors. Nature doesn't have categories. Language does.

wtf wrote: Tue Apr 30, 2019 11:03 pm The deeper error is that you misunderstand the type of objects that isomorphism applies to
We'll get to classification errors later.

### Re: Converting formal proofs to conform to sound deduction

Posted: Tue Apr 30, 2019 11:27 pm
Logik wrote: Tue Apr 30, 2019 11:23 pm
wtf wrote: Tue Apr 30, 2019 11:03 pm Really? So when I say "All cats are mammals" that's the same as saying cats are isomorphic to mammals?
OK. so you are using "are" to mean "subset of". Cool. We can play that game right until we get to the set of all sets.

And then I am going to ask you....
wtf wrote: Tue Apr 30, 2019 11:03 pm This isn't just wrong on the facts, it's meta-wrong. It's a category error.
Yep... How did you classify your first set. What is your first category?

wtf wrote: Tue Apr 30, 2019 11:03 pm The deeper error is that you misunderstand the type of objects that isomorphism applies to
We'll get to errors later.
Not picking a fight, just making an observation. Perhaps we have different "background frames" for the concept of isomorphism. I studied math and have a very precise mathematical and philosophical context for isomorphism. Perhaps you're thinking of something different.

I truly don't know what you mean by saying that "All cats are mammals" or even "All X are Y" is an example of an isomorphism. As I say that seems doubly wrong to me. But I'm not, you know, agitated about it. You seemed a little defensive here. Your other remarks seems a little off frankly. I don't want to hit them one by one because, stepping back here, I can see that we must be using certain words in very different ways. Like "isomorphism" and "cat."