There are infallible documents

[Dr Faustus]

You mean one which is not autoreferenced ?

No, I mean one which is necesasrily true.

If i produce a document where i say that, a=a, this is a valid document right ?

Not necessarily.

There exists a logic such that: For some x: x = x, for some y: MAYBE y = y; and for some z: z != z

Equality/identity is simply not well-defined.

https://en.wikipedia.org/wiki/Schr%C3%B6dinger_logic

Valid document are just those who respect logic rules

With respect to WHICH logic rules. There are infinitely many rule-based systems.

rules of identity, there is no big mistery inside it.

The mystery is why you believe in identity.

Real things does not always follow the images that we have of them in mind. That's a problem that logic can not really solve.

Logic doesn't even follow the image you have of it in your own head.

That's a problem you can't solve.

We need identity laws to construct knowledge about things. I read with Schrödinger's logic that it is not a logic without identity laws but with more restrictions on identity laws.

Identity laws are just tools.

Schrödinger logics are multi-sorted logics in which the expression x = y is not a well-formed formula in general.

[godelian]

Consider the proposition/theory: ∀T∀P (T⊨¬P)
Is this theory/proposition true or false?

The real problem is the expression "∀T", which is not recursively enumerable. So, the proposition may not be valid already on those grounds alone. But then again, assuming it were valid, it is still provably false by providing one, single counterexample theory T. That is exactly what ChatGPT did.

[Skepdick]

We need identity laws to construct knowledge about things. I read with Schrödinger's logic that it is not a logic without identity laws but with more restrictions on identity laws.

Identity laws are just tools.

I know that.

That doesn't make the choice of laws any less arbitrary.

Schrödinger logics are multi-sorted logics in which the expression x = y is not a well-formed formula in general.

I know that too.

x=y is not a well-formed formula in general, because the equality symbol is not a well-defined symbol in general.

And since equality is not well-defined, neither is the expression a=a.

[Skepdick]

Consider the proposition/theory: ∀T∀P (T⊨¬P)
Is this theory/proposition true or false?

The real problem is the expression "∀T", which is not recursively enumerable. So, the proposition may not be valid already on those grounds alone. But then again, assuming it were valid, it is still provably false by providing one, single counterexample theory T. That is exactly what ChatGPT did.

You have missed the forrest for the trees. Again.

Providing a single counter-example to ∀T∀P (T⊨¬P) proves PRECISELY the statement: For some T and some P (T ⊭ ¬P)

You've proven the negation of the entailment. Nothing more. Nothing less.

[Dr Faustus]

We need identity laws to construct knowledge about things. I read with Schrödinger's logic that it is not a logic without identity laws but with more restrictions on identity laws.

Identity laws are just tools.

I know that.

That doesn't make the choice of laws any less arbitrary.

Schrödinger logics are multi-sorted logics in which the expression x = y is not a well-formed formula in general.

I know that too.

x=y is not a well-formed formula in general, because the equality symbol is not a well-defined symbol in general.

And since equality is not well-defined, neither is the expression a=a.

The laws we use are made for the object we study. If it works, this not arbitrary.

But I agree with you, there are many problems with laws of identity.

[Skepdick]

The laws we use are made for the object we study. If it works, this not arbitrary.

"Works" is just a weasel word absent of a utility function.

But I agree with you, there are many problems with laws of identity.

They are abstract over-simplifications. With zero grounding in reality, except via our conceptual practices.

a=a works for the purposes of vacuous self-justification.

[Dr Faustus]

The laws we use are made for the object we study. If it works, this not arbitrary.

"Works" is just a weasel word absent of a utility function.

But I agree with you, there are many problems with laws of identity.

They are abstract over-simplifications. With zero grounding in reality, except via our conceptual practices.

a=a works for the purposes of vacuous self-justification.

Yes, utility function based on the reality that encounter humain kind.

[godelian]

You've proven the negation of the entailment. Nothing more. Nothing less.

The negation of the universal quantifier is an existential one.

In terms of mathematical logic, there exists truth because there is at least on theory that has at least one model that contains it. Therefore, the claim that there is no truth at all is mathematically false.

[Skepdick]

Yes, utility function based on the reality that encounter humain kind.

Utility functions are based on the users of reality, not on reality.

[Skepdick]

The negation of the universal quantifier is an existential one.

No, it isn't.

Existential quantification requires a witness.

To assume the negation of the universal quantifier entails an existential quantifier presupposes a universal model of logic where that inference rule always holds.

If such a model exists - produce it.

Instead, all you are going to produce is Classical logic (where the inference rule holds), while brushing Constructive logic under the carpet - because the inference rule doesn't hold.

Once again...
https://en.wikipedia.org/wiki/Rice%27s_theorem

A non-trivial property is one which is neither true for every program, nor false for every program.

In this case - the property which is Neither true nor false for every program is the inference rule "The negation of the universal quantifier implies an existential one."

In terms of mathematical logic, there exists truth because there is at least on theory that has at least one model that contains it. Therefore, the claim that there is no truth at all is mathematically false.

Which has what to do with providing the witness necessary for the existential quantifier?

[godelian]

You've proven the negation of the entailment. Nothing more. Nothing less.

I have proved the following: ¬(∀T∀P (T⊨¬P)) → (∃T∃P (T⊨P))

ChatGPT: ¬(∀T∀P (T⊨¬P)) → (∃T∃P (T⊨P))

The given logical statement is:

¬(∀T∀P(T⊨¬P))→(∃T∃P(T⊨P))

Let's break this down step by step.

Step 1: Understanding the Components

T⊨P means that the theory T semantically entails the proposition P.
T⊨¬P means that T semantically entails the negation of P.
∀T∀P(T⊨¬P) asserts that every theory T entails every proposition P in its negated form. This means that all propositions are false in every theory.
The negation of this statement, ¬(∀T∀P(T⊨¬P)), means that there exists at least one theory T and at least one proposition P for which T does not entail ¬P, i.e., T⊭¬P.

Step 2: Interpreting the Implication

The right-hand side of the implication states:

∃T∃P(T⊨P)

This means that there is at least one theory T and at least one proposition P such that T entails P.

Thus, the overall statement:

¬(∀T∀P(T⊨¬P))→(∃T∃P(T⊨P))

suggests that if it is not the case that every theory entails the negation of every proposition, then there must exist some theory that entails some proposition.

Step 3: Logical Intuition

This makes sense intuitively. If not every proposition is false in every theory, then at least one proposition must be true in some theory. In other words, if not everything is false, then something must be true. Thus, this formula expresses a fundamental principle of classical logic: if negation does not hold universally, then some positive assertion must hold somewhere.

Concerning ¬(∀T∀P (T⊨¬P)), all that is required is a witness theory T that allows for some truth in one of its models:

ChatGPT: ∀T∀P ( T ⊨ ¬P). Find an example theory for which this statement is false.

Counterexample: Consider the theory T={}, i.e., the empty theory, which contains no axioms. Take any proposition P, say P itself as a single atomic formula. Since T is empty, it imposes no constraints on P. In particular, there exist models where P is true and models where P is false. Thus, T⊭¬P because there exists at least one model of T in which P holds. Since we found a case where the universal quantification fails, the given logical statement is false.

This is a model-theoretically formalized alternative for: It is not possible that all propositions are false because in that case this very proposition is also false. Hence, there exist true propositions. This can be proven entirely in first-order logic. No need for a truth predicate or a metatheory. I concede, however, the problem caused by trying to recursively enumerate theories (∀T).

[godelian]

Existential quantification requires a witness.

As ChatGPT mentioned, the empty theory is a witness along with any arbitrary proposition.

Instead, all you are going to produce is Classical logic (where the inference rule holds), while brushing Constructive logic under the carpet - because the inference rule doesn't hold.

Okay, I assume the Law of the Excluded Middle, LEM, which indeed pushes the argument entirely into classical logic. This is not wrong. It just means that I must justify why the LEM would hold.

In this case - the property which is Neither true nor false for every program is the inference rule "The negation of the universal quantifier implies an existential one."

Okay, I admit the use of the LEM. I am still looking for a justification for that. Given the fact that it is constructivistically objectionable to do that, I am still working on a justification for using the LEM.

[Skepdick]

You've proven the negation of the entailment. Nothing more. Nothing less.

I have proved the following: ¬(∀T∀P (T⊨¬P)) → (∃T∃P (T⊨P))

No, You haven't.

Providing a witness for ¬(∀T∀P (T⊨¬P)) isn't the same as providing a witness for ¬(∀T∀P (T⊨¬P)) → (∃T∃P (T⊨P))

https://en.wikipedia.org/wiki/Brouwer%E ... rpretation

A proof of P → Q is a computable function f that converts a proof of P into a proof of Q

In a constructive setting, implications require explicit witness transformation procedures, not just truth value relationships.

[Skepdick]

As ChatGPT mentioned, the empty theory is a witness along with any arbitrary proposition.

Eh? An empty theory with a witness is an absurdity - a contradiction.

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

Okay, I assume the Law of the Excluded Middle, LEM, which indeed pushes the argument entirely into classical logic. This is not wrong. It just means that I must justify why the LEM would hold.

So do that before you use/apply it.

Okay, I admit the use of the LEM. I am still looking for a justification for that. Given the fact that it is constructivistically objectionable to do that, I am still working on a justification for using the LEM.

You won't find one. The computational formulation of LEM is the CHOICE() function.

The only reason you choose LEM is because you want to arrive at your conclusion. Which you can't do unless you assume LEM.

[godelian]

You've proven the negation of the entailment. Nothing more. Nothing less.

I have proved the following: ¬(∀T∀P (T⊨¬P)) → (∃T∃P (T⊨P))

No, You haven't.

Providing a witness for ¬(∀T∀P (T⊨¬P)) isn't the same as providing a witness for ¬(∀T∀P (T⊨¬P)) → (∃T∃P (T⊨P))

It is in classical logic. I agree, however, that there are constructivist concerns. I am still trying to figure out what to do with this concern. I am currently looking at how the constructivist version of the proof for Gödel's first incompleteness theorem was rephrased away from its original version in classical logic. It may contain a trick as to how to solve the problem.