No, I’m using common sense both to evaluate A() and as S. In sound common sense, A()≠2 does not imply (A()=2 ⇒ U()=3^^^3).
That’s because in common sense A()=2 ⇒ U()=1000 is true and provable, and (A()=2 ⇒ U()=1000) implies (A()=2 ⇒ U()≠3^^^3)), and in common sense (A()=2 ⇒ U()≠3^^^3)) and (A()=2 ⇒ U()=3^^^3)) are contradicting statements rather than proof that A()≠2.
The soundness of common sense is very much in dispute, except in the case of common sense along with some basic axioms of fully described formal systems- common sense with those added axioms is clearly unsound.
In sound common sense, A()≠2 does not imply (A()=2 ⇒ U()=3^^^3).
Okay, then I don’t know what kind of reasoning system this “common sense” is or how to build an inference system that implements it to put as S in A(). As a result, discussing it becomes unfruitful unless you give more details about what it is and/or motivation for considering it an interesting/relevant construction.
(What I wanted to point out in the grandparent is that the wrong conclusion can be completely explained by reasoning-from-outside being separate from S, without reasoning-from-outside losing any standard properties.)
No, I’m using common sense both to evaluate A() and as S. In sound common sense, A()≠2 does not imply (A()=2 ⇒ U()=3^^^3).
That’s because in common sense A()=2 ⇒ U()=1000 is true and provable, and (A()=2 ⇒ U()=1000) implies (A()=2 ⇒ U()≠3^^^3)), and in common sense (A()=2 ⇒ U()≠3^^^3)) and (A()=2 ⇒ U()=3^^^3)) are contradicting statements rather than proof that A()≠2.
The soundness of common sense is very much in dispute, except in the case of common sense along with some basic axioms of fully described formal systems- common sense with those added axioms is clearly unsound.
Okay, then I don’t know what kind of reasoning system this “common sense” is or how to build an inference system that implements it to put as S in A(). As a result, discussing it becomes unfruitful unless you give more details about what it is and/or motivation for considering it an interesting/relevant construction.
(What I wanted to point out in the grandparent is that the wrong conclusion can be completely explained by reasoning-from-outside being separate from S, without reasoning-from-outside losing any standard properties.)