Transforming formal proof into sound deduction (greatly simplified)
-
- Posts: 1514
- Joined: Mon Jul 25, 2016 6:55 pm
Transforming formal proof into sound deduction (greatly simplified)
Within the sound deductive inference model there is a (connected sequence of valid deductions from true premises to a true conclusion) unlike the formal proofs of symbolic logic provability cannot diverge from truth.
When we consider sound deductive inference to the negation of a conclusion we now also have a definitive specification of falsity.
Within the sound deductive inference model we can be certain that valid inference from true premises derives a true conclusion.
∴ Within the sound deductive inference model any logic sentence that does not evaluate to True or False is unsound, there is no undecidability or incompleteness in this model.
The key criterion measure that the sound deductive inference model would add to the formal proofs to theorem consequences of symbolic logic would be the semantic notion of soundness.
When we consider sound deductive inference to the negation of a conclusion we now also have a definitive specification of falsity.
Within the sound deductive inference model we can be certain that valid inference from true premises derives a true conclusion.
∴ Within the sound deductive inference model any logic sentence that does not evaluate to True or False is unsound, there is no undecidability or incompleteness in this model.
The key criterion measure that the sound deductive inference model would add to the formal proofs to theorem consequences of symbolic logic would be the semantic notion of soundness.
Last edited by PeteOlcott on Mon Apr 22, 2019 10:23 pm, edited 1 time in total.
-
- Posts: 4365
- Joined: Wed Feb 10, 2010 2:04 pm
Re: Transforming formal proof into sound deduction (greatly simplified)
defining the future does not ensure its conformity to your definition...
-Imp
-Imp
-
- Posts: 1514
- Joined: Mon Jul 25, 2016 6:55 pm
Re: Transforming formal proof into sound deduction (greatly simplified)
You are failing to understand the Analytic/Synthetic distinction:Impenitent wrote: ↑Mon Apr 22, 2019 4:02 pm defining the future does not ensure its conformity to your definition...
-Imp
https://plato.stanford.edu/entries/analytic-synthetic/
Re: Transforming formal proof into sound deduction (greatly simplified)
And you are failing to understand that not everybody subscribes to Kantian philosophy. Unless they choose to.PeteOlcott wrote: ↑Tue Apr 23, 2019 4:56 am You are failing to understand the Analytic/Synthetic distinction:
https://plato.stanford.edu/entries/analytic-synthetic/
-
- Posts: 1514
- Joined: Mon Jul 25, 2016 6:55 pm
Re: Transforming formal proof into sound deduction (greatly simplified)
Truth is the way that it is, one either gets this correctly or fails to. Mathematical specifications such as mine are eternal.Logik wrote: ↑Tue Apr 23, 2019 11:17 amAnd you are failing to understand that not everybody subscribes to Kantian philosophy. Unless they choose to.PeteOlcott wrote: ↑Tue Apr 23, 2019 4:56 am You are failing to understand the Analytic/Synthetic distinction:
https://plato.stanford.edu/entries/analytic-synthetic/
Re: Transforming formal proof into sound deduction (greatly simplified)
That is a rather interesting decision problem unfolding right before you.PeteOlcott wrote: ↑Tue Apr 23, 2019 2:56 pm Truth is the way that it is, one either gets this correctly or fails to.
We have two hypothesis on the table:
A. Pete Olcott correctly gets the way truth is.
B. Pete Olcott fails to get the way truth is.
In what formal system would you decide whether A ⇔ True, B ⇔ False; OR A ⇔ False, B ⇔ True
-
- Posts: 1514
- Joined: Mon Jul 25, 2016 6:55 pm
Re: Transforming formal proof into sound deduction (greatly simplified)
Truth is what it is no matter who thinks otherwise.Logik wrote: ↑Tue Apr 23, 2019 3:08 pmThat is a rather interesting decision problem unfolding right before you.PeteOlcott wrote: ↑Tue Apr 23, 2019 2:56 pm Truth is the way that it is, one either gets this correctly or fails to.
We have two hypothesis on the table:
A. Pete Olcott correctly gets the way truth is.
B. Pete Olcott fails to get the way truth is.
In what formal system would you decide whether A ⇔ True, B ⇔ False; OR A ⇔ False, B ⇔ True
Wrongheaded opinions have no effect on the actual nature of truth itself what-so-ever.
The only reliable formal system to determine what is true and what is false
with 100% perfectly justified complete certainty is the sound deductive inference model.
Re: Transforming formal proof into sound deduction (greatly simplified)
Well well, we have ourselves an idealist.PeteOlcott wrote: ↑Tue Apr 23, 2019 4:00 pmTruth is what it is no matter who thinks otherwise.Logik wrote: ↑Tue Apr 23, 2019 3:08 pmThat is a rather interesting decision problem unfolding right before you.PeteOlcott wrote: ↑Tue Apr 23, 2019 2:56 pm Truth is the way that it is, one either gets this correctly or fails to.
We have two hypothesis on the table:
A. Pete Olcott correctly gets the way truth is.
B. Pete Olcott fails to get the way truth is.
In what formal system would you decide whether A ⇔ True, B ⇔ False; OR A ⇔ False, B ⇔ True
Wrongheaded opinions have no effect on the actual nature of truth itself what-so-ever.
The only reliable formal system to determine what is true and what is false
with 100% perfectly justified complete certainty is the sound deductive inference model.
Great.
So you will help us get to the "100% justified completely certain truth"
Either
"Pete Olcott correctly gets the way truth is" ⇔ True
OR
Pete Olcott fails to get the way truth is." ⇔ True
And since you absolutely INSIST that: ¬(True ⇔ False) then I guess one of the options above is 100% true and correct; and the other is 100% false and incorrect.
Please help us decide.
-
- Posts: 1514
- Joined: Mon Jul 25, 2016 6:55 pm
Re: Transforming formal proof into sound deduction (greatly simplified)
https://en.wikipedia.org/wiki/Stipulative_definitionLogik wrote: ↑Tue Apr 23, 2019 4:05 pmWell well, we have ourselves an idealist.PeteOlcott wrote: ↑Tue Apr 23, 2019 4:00 pmTruth is what it is no matter who thinks otherwise.Logik wrote: ↑Tue Apr 23, 2019 3:08 pm
That is a rather interesting decision problem unfolding right before you.
We have two hypothesis on the table:
A. Pete Olcott correctly gets the way truth is.
B. Pete Olcott fails to get the way truth is.
In what formal system would you decide whether A ⇔ True, B ⇔ False; OR A ⇔ False, B ⇔ True
Wrongheaded opinions have no effect on the actual nature of truth itself what-so-ever.
The only reliable formal system to determine what is true and what is false
with 100% perfectly justified complete certainty is the sound deductive inference model.
Great.
So you will help us get to the "100% justified completely certain truth"
Either
"Pete Olcott correctly gets the way truth is" ⇔ True
OR
Pete Olcott fails to get the way truth is." ⇔ True
And since you absolutely INSIST that: ¬(True ⇔ False) then I guess one of the options above is 100% true and correct; and the other is 100% false and incorrect.
Please help us decide.
A stipulative definition is a type of definition in which a new or
currently-existing term is given a new specific meaning for the
purposes of argument or discussion in a given context.
I am stipulating:
T ⇔ True
⊥ ⇔ False
I am also stipulating that all of the definitions and relations of predicate logic.
Re: Transforming formal proof into sound deduction (greatly simplified)
Aristotle did that 2000 years ago.PeteOlcott wrote: ↑Tue Apr 23, 2019 4:41 pm https://en.wikipedia.org/wiki/Stipulative_definition
A stipulative definition is a type of definition in which a new or
currently-existing term is given a new specific meaning for the
purposes of argument or discussion in a given context.
I am stipulating:
T ⇔ True
⊥ ⇔ False
I am also stipulating that all of the definitions and relations of predicate logic.
Don't you feel like you are stealing Stanford's money after 22 years ?
-
- Posts: 1514
- Joined: Mon Jul 25, 2016 6:55 pm
Re: Transforming formal proof into sound deduction (greatly simplified)
I closed the expressiveness gap of formal proofs to theorem consequences of symbolic logicLogik wrote: ↑Tue Apr 23, 2019 4:43 pmAristotle did that 2000 years ago.PeteOlcott wrote: ↑Tue Apr 23, 2019 4:41 pm https://en.wikipedia.org/wiki/Stipulative_definition
A stipulative definition is a type of definition in which a new or
currently-existing term is given a new specific meaning for the
purposes of argument or discussion in a given context.
I am stipulating:
T ⇔ True
⊥ ⇔ False
I am also stipulating that all of the definitions and relations of predicate logic.
Don't you feel like you are stealing Stanford's money after 22 years ?
by converting these formal proofs to conform to the sound deductive inference model.
Re: Transforming formal proof into sound deduction (greatly simplified)
In my personal experience rules hinder expressiveness, but lets skip that for a second.PeteOlcott wrote: ↑Tue Apr 23, 2019 4:58 pm I closed the expressiveness gap of formal proofs to theorem consequences of symbolic logic
by converting these formal proofs to conform to the sound deductive inference model.
In what way is the deductive inference model different to proof theory?
-
- Posts: 1514
- Joined: Mon Jul 25, 2016 6:55 pm
Re: Transforming formal proof into sound deduction (greatly simplified)
Undecidability, and incompleteness cannot exist in the former.Logik wrote: ↑Tue Apr 23, 2019 5:06 pmIn my personal experience rules hinder expressiveness, but lets skip that for a second.PeteOlcott wrote: ↑Tue Apr 23, 2019 4:58 pm I closed the expressiveness gap of formal proofs to theorem consequences of symbolic logic
by converting these formal proofs to conform to the sound deductive inference model.
In what way is the deductive inference model different to proof theory?
When redefining formal proofs to conform to sound deduction the incompleteness theorem is refuted.
Re: Transforming formal proof into sound deduction (greatly simplified)
Aren't there mutually exclusive but independently self-consistent axiomatic systems?PeteOlcott wrote: ↑Mon Apr 22, 2019 6:47 am Within the sound deductive inference model there is a (connected sequence of valid deductions from true premises to a true conclusion) unlike the formal proofs of symbolic logic provability cannot diverge from truth.
For example the axioms of geometry with the parallel postulate, and the axioms of geometry without the parallel postulate.
I still don't understand how you deal with that situation.
In my understanding of the terms, a deduction in Euclidean or non-Euclidean geometry can be valid, meaning it goes from premises to conclusion by a legal sequence of applications of the inference rules.
But neither system can be said by logicians or geometers to be true. That question is a matter for the physicists.
-
- Posts: 1514
- Joined: Mon Jul 25, 2016 6:55 pm
Re: Transforming formal proof into sound deduction (greatly simplified)
https://www.cs.unm.edu/~joel/NonEuclid/ ... idean.htmlwtf wrote: ↑Wed Apr 24, 2019 2:20 amAren't there mutually exclusive but independently self-consistent axiomatic systems?PeteOlcott wrote: ↑Mon Apr 22, 2019 6:47 am Within the sound deductive inference model there is a (connected sequence of valid deductions from true premises to a true conclusion) unlike the formal proofs of symbolic logic provability cannot diverge from truth.
For example the axioms of geometry with the parallel postulate, and the axioms of geometry without the parallel postulate.
I still don't understand how you deal with that situation.
In my understanding of the terms, a deduction in Euclidean or non-Euclidean geometry can be valid, meaning it goes from premises to conclusion by a legal sequence of applications of the inference rules.
But neither system can be said by logicians or geometers to be true. That question is a matter for the physicists.
That took me almost five minutes to figure out.
Most of the time was finding out the details of Non-Euclidean Geometry.
My system already handles that by defining truth to be relative to a formal system:
Axiom(1) ∀F ∈ Formal_System ∀x ∈ Closed_WFF(F) (True(F, x) ↔ (F ⊢ x))
Axiom(2) ∀F ∈ Formal_System ∀x ∈ Closed_WFF(F) (False(F, x) ↔ (F ⊢ ¬x))