Converting formal proofs to conform to sound deduction

 Posts: 970
 Joined: Mon Jul 25, 2016 6:55 pm
Converting formal proofs to conform to sound deduction
This post requires some knowledge of the terminology of formal proofs of symbolic logic.
In the same way that not all finite strings are wellformed
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.
In the same way that not all finite strings are wellformed
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
You have successfully managed to hide the ball from yourself again.PeteOlcott wrote: ↑Tue Apr 30, 2019 4:03 pmThis post requires some knowledge of the terminology of formal proofs of symbolic logic.
In the same way that not all finite strings are wellformed
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.
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 Turingcompleteness.

 Posts: 970
 Joined: Mon Jul 25, 2016 6:55 pm
Re: Converting formal proofs to conform to sound deduction
https://www.researchgate.net/publicatio ... y_YACC_BNFLogik wrote: ↑Tue Apr 30, 2019 5:01 pmYou have successfully managed to hide the ball from yourself again.PeteOlcott wrote: ↑Tue Apr 30, 2019 4:03 pmThis post requires some knowledge of the terminology of formal proofs of symbolic logic.
In the same way that not all finite strings are wellformed
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.
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 Turingcompleteness.
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 metalanguage 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
So the MTT language is NOT Turing complete? How do you do shortestpath traversal of the DAG?PeteOlcott wrote: ↑Tue Apr 30, 2019 5:45 pmMTT is a universal Tarski metalanguage that can represent the semantics of any expression
of any formal system, including its own semantics as a directed acyclic graph (DAG).
And if MTT IS Turingcomplete, 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?

 Posts: 970
 Joined: Mon Jul 25, 2016 6:55 pm
Re: Converting formal proofs to conform to sound deduction
MTT has an isomorphism to lambda calculus.Logik wrote: ↑Tue Apr 30, 2019 5:49 pmSo the MTT language is NOT Turing complete? How do you do shortestpath traversal of the DAG?PeteOlcott wrote: ↑Tue Apr 30, 2019 5:45 pmMTT is a universal Tarski metalanguage that can represent the semantics of any expression
of any formal system, including its own semantics as a directed acyclic graph (DAG).
And if MTT IS Turingcomplete, 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 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
These two claims are incompatible with each other.PeteOlcott wrote: ↑Tue Apr 30, 2019 6:48 pmMTT is consistent and complete and will not allow introducing any axioms conflicting with its current axioms.
If MTT is Turing complete then any and all notions of "formal proof" are isomorphic to algorithms as per CurryHoward 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 Turingcomplete system, I control the system. I can make it sing the Star Spangled banner if I want to.

 Posts: 970
 Joined: Mon Jul 25, 2016 6:55 pm
Re: Converting formal proofs to conform to sound deduction
MTT the formal language will let you do anything that lambda calculus will allow.Logik wrote: ↑Tue Apr 30, 2019 7:36 pmThese two claims are incompatible with each other.PeteOlcott wrote: ↑Tue Apr 30, 2019 6:48 pmMTT is consistent and complete and will not allow introducing any axioms conflicting with its current axioms.
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
PeteOlcott wrote: ↑Tue Apr 30, 2019 8:11 pmMTT 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?!?

 Posts: 970
 Joined: Mon Jul 25, 2016 6:55 pm
Re: Converting formal proofs to conform to sound deduction
This system is already populated with the complete set of human common sense:Logik wrote: ↑Tue Apr 30, 2019 8:17 pmPeteOlcott wrote: ↑Tue Apr 30, 2019 8:11 pmMTT 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?!?
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
I call bullshit that you can fit all knowledge from the Internet into one consistent system, but lets go with that for 2 seconds.PeteOlcott wrote: ↑Tue Apr 30, 2019 8:36 pmThis system is already populated with the complete set of human common sense:
https://en.wikipedia.org/wiki/Cyc
I'll even pretend that you have (somehow) figured out how to unify incompatible theories like General Relativity and Quantum Mechanics.
wtf already showed you a mathematical framework in which 1 = 0 is a perfectly valid expression.PeteOlcott wrote: ↑Tue Apr 30, 2019 8:36 pmIf 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.
So I ask again. WHO chose the axioms and why? Because their "common sense" clearly disagrees with my "common sense".

 Posts: 970
 Joined: Mon Jul 25, 2016 6:55 pm
Re: Converting formal proofs to conform to sound deduction
This is also perfectly valid, it is, however, unsound:Logik wrote: ↑Tue Apr 30, 2019 8:47 pmI call bullshit that you can fit all knowledge from the Internet into one consistent system, but lets go with that for 2 seconds.PeteOlcott wrote: ↑Tue Apr 30, 2019 8:36 pmThis system is already populated with the complete set of human common sense:
https://en.wikipedia.org/wiki/Cyc
I'll even pretend that you have (somehow) figured out how to unify incompatible theories like General Relativity and Quantum Mechanics.
wtf already showed you a mathematical framework in which 1 = 0 is a perfectly valid expression.PeteOlcott wrote: ↑Tue Apr 30, 2019 8:36 pmIf 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.
So I ask again. WHO chose the axioms and why? Because their "common sense" clearly disagrees with my "common sense".
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.
Last edited by PeteOlcott on Wed May 01, 2019 12:04 am, edited 1 time in total.
Re: Converting formal proofs to conform to sound deduction
It's an Idiotic example because you have absolutely no way of introducing modal logic into your ontology.PeteOlcott wrote: ↑Tue Apr 30, 2019 8:51 pmThis 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
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 counterexample to your deductive rule renders your deduction invalid.
You have no absolute truths in this universe.. You have no realworld objects/phenomena/things for which you can universally say ALL X are Y.
None. Nada. Zero.
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
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 metawrong. 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 settheoretic objects that are not the same set at all. But there's a structurepreserving 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.
Last edited by wtf on Tue Apr 30, 2019 11:23 pm, edited 1 time in total.
Re: Converting formal proofs to conform to sound deduction
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....
...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.
We'll get to classification errors later.
Re: Converting formal proofs to conform to sound deduction
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."
Who is online
Users browsing this forum: No registered users and 3 guests