“we find out that we used the axiom true(QUOT[ought(X)]) ⇔ ought(X) from the schema. So in order to derive ought(X), we still had to use an axiom with “ought” in it.”
But that “axiom”, as you call it, is trivially true, as it follows from any sensible definition or understanding of “true”. In particular, it follows from the axiom “true(QUOT[X]) ⇔ X”, which doesn’t have an ought in it.
Moreover, we don’t even need the true predicate in this argument (we can formulate it in the spirit of the deflationary theory of truth):
2′. Whenever John says that X, then X. ( ∀ s:proposition, says(John, s) ⇒ s )
I think the issue boils down to one of types and not being able to have a “Statement” type in the theory. This is why we have QUOT[X] to convert a statement X into a string.QUOT is not a function, really, it’s a macro that converts a statement into a string representation of that statement.true(QUOT[X]) ⇔ X isn’t an axiom, it’s an infinite sequence of axioms (a “schema”), one for each possible statement X. It’s considered okay to have an infinite sequence of axioms, so long as you know how to compute that sequence. We can enumerate through all possible statements X, and we know how to convert any of those statements into a string using QUOT, so that’s all okay. But we can’t boil down that infinite axiom schema into a single axiom ∀ S:Statement, true(quot(S)) ⇒ S because we don’t have a Statement type inside of the system.
Why can’t we have a Statement type? Well, we could if they were just constants that took on values of “true” or “false”. But, I think what you want to do here is treat statements as both sequences of symbols and as things that can directly be true or false. Then the reasoning system would have ways of combining the sequences of symbols and axioms that map to rules of inference on those symbols.
Imagine what would happen if we did have all those things. I’ll define a notation for a statement literal as state(s), where s is the string of symbols that make up the statement. So state() is kind of an inverse of QUOT[], except that it’s a proper function, not a macro. Since not all strings might form valid statements, we’ll take state(s) to return some default statement like false when s is not valid.
Here is the paradox. We could construct the statement: ∀ S:Statement, ∀ fmtstr:String,(fmtstr = "..." ⇒ (S = state(replace(fmtstr, "%s", repr(fmtstr))) ⇒ ¬S)) where the "..." is "∀ S:Statement, ∀ fmtstr:String,(fmtstr = %s ⇒ (S = state(replace(fmtstr, \"\%s\", repr(fmtstr))) ⇒ ¬S))" So written out in full, the statement would be:
Now consider the statement itself as S in the quantifier, and suppose that fmtstr is indeed equal to "...". Then S = state(replace(fmtstr, "%s", repr(fmtstr))) is true. Then we have ¬S. On the other hand, if S or fmtstr take other values, then the conditional implications become vacuously true. So S reduces down entirely to ¬S. This is a contradiction. Not the friendly quine-based paradox of Godel’s incompleteness theorem, which merely asserts provability, but an actual logic-exploding contradiction.
Therefore we can’t allow a Statement type in our logic.
2′. Whenever John says that X, then X. ( ∀ X:proposition, says(John, X) ⇒ X )
Note that X here is not a statement (grammatically valid sentence?), but a proposition. John can express it however he likes: by means of written word, by means of a demonstration or example, by means of a telepathy, etc. There is no need, specifically, to convert a proposition to a string or vice versa; as long as (1) is true and we most likely understand what proposition John is trying to convey, we will most likely believe in the correct normative proposition (that, if expressed in a statement, requires an “ought”).
Ugh, you are using the language of programming in an area where it doesn’t fit. Can you explain what are these funny backslashes, % signs etc.? Why did you name a variable fmtstr instead of simply X?
Anyway—statements obviously exist, so if your theory doesn’t allow for them, it’s the problem with your theory and we can just ignore it. In my theory, every sentence that corresponds to a proposition (not all do of course), if that sentence is utterred by John, that proposition is true—that’s what I mean by John being truthful. There is no additional axiom here, this is just premise 2, rephrased.
Just to give you some (very late) clarification: The theory I describe above (a first order theory) can handle statements perfectly well, it just represents them as strings, rather than giving them their own separate type. The problem isn’t inherently with giving them their own separate type though, it’s with expecting to be able to just stick a member of that type in our expression where we’re supposed to expect a truth value.
You can skip past my proof and its messy programming notation, and just look here.
“we find out that we used the axiom
true(QUOT[ought(X)]) ⇔ ought(X)from the schema. So in order to deriveought(X), we still had to use an axiom with “ought” in it.”But that “axiom”, as you call it, is trivially true, as it follows from any sensible definition or understanding of “true”. In particular, it follows from the axiom “
true(QUOT[X]) ⇔ X”, which doesn’t have an ought in it.Moreover, we don’t even need the true predicate in this argument (we can formulate it in the spirit of the deflationary theory of truth):
2′. Whenever John says that X, then X. ( ∀ s:proposition, says(John, s) ⇒ s )
I think the issue boils down to one of types and not being able to have a “Statement” type in the theory. This is why we have
QUOT[X]to convert a statementXinto a string.QUOTis not a function, really, it’s a macro that converts a statement into a string representation of that statement.true(QUOT[X]) ⇔ Xisn’t an axiom, it’s an infinite sequence of axioms (a “schema”), one for each possible statementX. It’s considered okay to have an infinite sequence of axioms, so long as you know how to compute that sequence. We can enumerate through all possible statementsX, and we know how to convert any of those statements into a string usingQUOT, so that’s all okay. But we can’t boil down that infinite axiom schema into a single axiom∀ S:Statement, true(quot(S)) ⇒ Sbecause we don’t have aStatementtype inside of the system.Why can’t we have a
Statementtype? Well, we could if they were just constants that took on values of “true” or “false”. But, I think what you want to do here is treat statements as both sequences of symbols and as things that can directly be true or false. Then the reasoning system would have ways of combining the sequences of symbols and axioms that map to rules of inference on those symbols.Imagine what would happen if we did have all those things. I’ll define a notation for a statement literal as
state(s), wheresis the string of symbols that make up the statement. Sostate()is kind of an inverse ofQUOT[], except that it’s a proper function, not a macro. Since not all strings might form valid statements, we’ll takestate(s)to return some default statement likefalsewhensis not valid.Here is the paradox. We could construct the statement:
∀ S:Statement, ∀ fmtstr:String,(fmtstr = "..." ⇒ (S = state(replace(fmtstr, "%s", repr(fmtstr))) ⇒ ¬S))where the"..."is"∀ S:Statement, ∀ fmtstr:String,(fmtstr = %s ⇒ (S = state(replace(fmtstr, \"\%s\", repr(fmtstr))) ⇒ ¬S))"So written out in full, the statement would be:∀ S:Statement, ∀ fmtstr:String,(fmtstr = "∀ S:Statement, ∀ fmtstr:String,(fmtstr = %s ⇒ (S = state(replace(fmtstr, \"\%s\", repr(fmtstr))) ⇒ ¬S))" ⇒ (S = state(replace(fmtstr, "%s", repr(fmtstr))) ⇒ ¬S))Now consider the statement itself as
Sin the quantifier, and suppose that fmtstr is indeed equal to"...". ThenS = state(replace(fmtstr, "%s", repr(fmtstr)))is true. Then we have¬S. On the other hand, ifSorfmtstrtake other values, then the conditional implications become vacuously true. SoSreduces down entirely to¬S. This is a contradiction. Not the friendly quine-based paradox of Godel’s incompleteness theorem, which merely asserts provability, but an actual logic-exploding contradiction.Therefore we can’t allow a
Statementtype in our logic.Oh, an one more thing. My updated premise 2 is:
2′. Whenever John says that X, then X. ( ∀ X:proposition, says(John, X) ⇒ X )
Note that X here is not a statement (grammatically valid sentence?), but a proposition. John can express it however he likes: by means of written word, by means of a demonstration or example, by means of a telepathy, etc. There is no need, specifically, to convert a proposition to a string or vice versa; as long as (1) is true and we most likely understand what proposition John is trying to convey, we will most likely believe in the correct normative proposition (that, if expressed in a statement, requires an “ought”).
Ugh, you are using the language of programming in an area where it doesn’t fit. Can you explain what are these funny backslashes, % signs etc.? Why did you name a variable fmtstr instead of simply X?
Anyway—statements obviously exist, so if your theory doesn’t allow for them, it’s the problem with your theory and we can just ignore it. In my theory, every sentence that corresponds to a proposition (not all do of course), if that sentence is utterred by John, that proposition is true—that’s what I mean by John being truthful. There is no additional axiom here, this is just premise 2, rephrased.
Just to give you some (very late) clarification: The theory I describe above (a first order theory) can handle statements perfectly well, it just represents them as strings, rather than giving them their own separate type. The problem isn’t inherently with giving them their own separate type though, it’s with expecting to be able to just stick a member of that type in our expression where we’re supposed to expect a truth value.
You can skip past my proof and its messy programming notation, and just look here.