Transforming formal proof into sound deduction (greatly simplified)

[PeteOlcott]

Every element of all of analytic truth is essentially stipulated as true and it
it only the stipulation that makes it true it is not true for any other reason.

nice circles.

as I said, defining the future does not ensure its conformity to your definition...

-Imp

When you define the future to be 5 > 3, (and other tautologies) then YES IT DOES !!!

It is not a circle it is an acyclic directed graph knowledge ontology:
https://www.cyc.com/wp-content/uploads/ ... base-1.png

[Logik]

It is not a circle it is an acyclic directed graph knowledge ontology:
https://www.cyc.com/wp-content/uploads/ ... base-1.png

What if I don't like your ontology and substitute my own?

https://en.wikipedia.org/wiki/Digital_philosophy

[PeteOlcott]

It is not a circle it is an acyclic directed graph knowledge ontology:
https://www.cyc.com/wp-content/uploads/ ... base-1.png

What if I don't like your ontology and substitute my own?

https://en.wikipedia.org/wiki/Digital_philosophy

https://en.wikipedia.org/wiki/Stipulative_definition
That would ONLY show that you fail to comprehend the idea of a stipulative definition
and thus are only interested in playing heads games and not in any actual dialogue.

[Logik]

https://en.wikipedia.org/wiki/Stipulative_definition
That would ONLY show that you fail to comprehend the idea of a stipulative definition
and thus are only interested in playing heads games and not in any actual dialogue.

Bullshit.

a stipulative definition cannot be "correct" or "incorrect"; it can only differ from other definitions, but it can be useful for its intended purpose.

You are yet to state any intent to the definitions you are stipulating. You are yet to state a utility function.

Formalism for its own sake is neither a clear purpose nor is it very useful.

[PeteOlcott]

https://en.wikipedia.org/wiki/Stipulative_definition
That would ONLY show that you fail to comprehend the idea of a stipulative definition
and thus are only interested in playing heads games and not in any actual dialogue.

Bullshit.

a stipulative definition cannot be "correct" or "incorrect"; it can only differ from other definitions, but it can be useful for its intended purpose.

You are yet to state any intent to the definitions you are stipulating.

Formalism for its own sake is circular.

It is like a "given" in geometry, the basis for subsequent dialogue.

Formalizing the Sound Deductive Inference Model in Symbolic Logic
Axiom(0) Stipulates** this definition of Axiom:
Expressions of language defined to have the semantic value of Boolean True.
Provides the symbolic logic equivalent of true premises.

Stipulating** this specification of True and False: (TRUE ↔ ⊤ ∧ FALSE ↔ ⊥)
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))
Thus stipulating** that consequences are provable from axioms.

Stipulating** that formal systems are Boolean:
Axiom(3) ∀F ∈ Formal_System ∀x ∈ Closed_WFF(F) (True(F,x) ∨ False(F,x))
Screens out semantically unsound sentences as not belonging to the formal system.
Applying the Formalized Sound Deductive Inference Model

[Logik]

Expressions of language defined to have the semantic value of Boolean True.
Provides the symbolic logic equivalent of true premises.

And I can take this claim and state that it's equivalent to the process of binary classification

Binary or binomial classification is the task of classifying the elements of a given set into two groups (predicting which group each one belongs to) on the basis of a classification rule. Contexts requiring a decision as to whether or not an item has some qualitative property, some specified characteristic

And so, given a mixed bag of linguistic expressions (Claims? Propositions? Axioms?) which could be true OR false, the task before you is to classify them correctly into the categories of: {True, False}

Let S be any sentence, claim, proposition or axiom.
Let C() be the binomial truth-classifier.

C(S) -> {True, False}

This is the standard form of the decision problem!

The classification rule to ANY binomial classification is isomorphic to an algorithm!

[Logik]

Perhaps you would spare yourself a lot of effort if you drew a distinction between intuitionistic fuzzy logic and neutrosophic logic

https://arxiv.org/ftp/math/papers/0303/0303009.pdf

[PeteOlcott]

Perhaps you would spare yourself a lot of effort if you drew a distinction between intuitionistic fuzzy logic and neutrosophic logic

https://arxiv.org/ftp/math/papers/0303/0303009.pdf

I see that you are persistently unable to stay in topic. I will estimate that
the reason for this is that I am saying things that are too difficult for you to understand.

The topic is converting the formal proofs of symbolic logic to conform
to the sound deductive inference mode. Everything else is off topic.

This paper is in nearly final form now after 22 years of research. I provide it as a supplement.
https://www.researchgate.net/publicatio ... al_Systems

[PeteOlcott]

Expressions of language defined to have the semantic value of Boolean True.
Provides the symbolic logic equivalent of true premises.

And I can take this claim and state that it's equivalent to the process of binary classification

Binary or binomial classification is the task of classifying the elements of a given set into two groups (predicting which group each one belongs to) on the basis of a classification rule. Contexts requiring a decision as to whether or not an item has some qualitative property, some specified characteristic

And so, given a mixed bag of linguistic expressions (Claims? Propositions? Axioms?) which could be true OR false, the task before you is to classify them correctly into the categories of: {True, False}

Let S be any sentence, claim, proposition or axiom.
Let C() be the binomial truth-classifier.

C(S) -> {True, False}

This is the standard form of the decision problem!

The classification rule to ANY binomial classification is isomorphic to an algorithm!

I am only dealing with sound deductive inference if you snuck any
inductive inference in there it is strictly off topic.

Some decision problems are analogous to this question:
What time is it (Yes or No) thus providing a third alternative.
It is this third alternative that is detected and rejected by my system.

These are not undecidable they are semantically unsound:
LP ↔ ¬True(LP)
G ↔ (⊬G)

[Logik]

Some decision problems are analogous to this question:
What time is it (Yes or No) thus providing a third alternative.
It is this third alternative that is detected and rejected by my system.

OK. Good luck to you.

Implement your error-detection mechanism in a programming language of your choosing.

I will happily show you why it doesn't work in practice. And I will tell you how I intend to: if your language is Turing-complete I will bootstrap myself into Python/Ruby and I will simply bypass your detection mechanism.

Or you are welcome to waste another 20 years of your life writing papers.

It's not my understanding that's the problem. It's yours. You don't grasp Kleene's realizability

[PeteOlcott]

Some decision problems are analogous to this question:
What time is it (Yes or No) thus providing a third alternative.
It is this third alternative that is detected and rejected by my system.

OK. Good luck to you.

Implement your error-detection mechanism in a programming language of your choosing.

I will happily show you why it doesn't work in practice. And I will tell you how I intend to: if your language is Turing-complete I will bootstrap myself into Python/Ruby and I will simply bypass your detection mechanism.

Or you are welcome to waste another 20 years of your life writing papers.

It's not my understanding that's the problem. It's yours. You don't grasp Kleene's realizability

You can show how the sound deductive logical inference model is either incomplete or inconsistent?

[Logik]

You can show how the sound deductive logical inference model is either incomplete or inconsistent?

"incompleteness" and "inconsistency" are synthetic notions. Formalize them.

Synthetic "truth" is off topic:
The ONLY thing that we can know for certain about reality is that it seems to be a
continuous stream of physical sensations. Everything else about reality is pure speculation.

Much like you claim that you have built a system which detects undecidability, produce a system which detects incompleteness and inconsistency in other systems.

[PeteOlcott]

You can show how the sound deductive logical inference model is either incomplete or inconsistent?

"incompleteness" and "inconsistency" are synthetic notions. Formalize them.

You are using the wrong meaning of synthetic. You are not using the one from philosophy.
The one from philosophy corresponds to Kant's a posteriori.

Here is consistency and completeness formalized:
Formalizing the Sound Deductive Inference Model in Symbolic Logic
Axiom(0) Stipulates** this definition of Axiom:
Expressions of language defined to have the semantic value of Boolean True.
Provides the symbolic logic equivalent of true premises.

Stipulating** this specification of True and False: (TRUE ↔ ⊤ ∧ FALSE ↔ ⊥)
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))
Thus stipulating** that consequences are provable from axioms.

Stipulating** that formal systems are Boolean:
Axiom(3) ∀F ∈ Formal_System ∀x ∈ Closed_WFF(F) (True(F,x) ∨ False(F,x))
Screens out semantically unsound sentences as not belonging to the formal system.

[Logik]

You are using the wrong meaning of synthetic. You are not using the one from philosophy.
The one from philosophy corresponds to Kant's a posteriori.

You are using the wrong meaning of "wrong". You are not using the one from Logik's philosophy.
The one from Logik's philosophy corresponds to a decision problem.

Please provide the proof for your sound deduction by which you determined that I am using the "wrong" meaning.

How quickly you have forgotten.
https://en.wikipedia.org/wiki/Stipulative_definition

a stipulative definition cannot be "correct" or "incorrect"; it can only differ from other definitions

[Logik]

Axiom(0) Stipulates** this definition of Axiom:
Expressions of language defined to have the semantic value of Boolean True.
Provides the symbolic logic equivalent of true premises.

Stipulating** this specification of True and False: (TRUE ↔ ⊤ ∧ FALSE ↔ ⊥)
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))
Thus stipulating** that consequences are provable from axioms.

Stipulating** that formal systems are Boolean:
Axiom(3) ∀F ∈ Formal_System ∀x ∈ Closed_WFF(F) (True(F,x) ∨ False(F,x))
Screens out semantically unsound sentences as not belonging to the formal system.

Also. I can't parse any of that. It's in some made up language that I don't care to learn.

Write it in C++.

I am most interested in these functions:

True()
False()
Closed_WFF()
↔()
∈()