Common sense proves that A()=1 easily, which implies A()≠2, but in sound common sense, A()≠2 does not imply (A()=2 ⇒ U()=3^^^3).
It does imply that. What happens is that you (in “common sense” system) don’t prove A()=2 as a consequence of proving (say) both (A()=1 ⇒ U()=1000000) and (A()=2 ⇒ U()=3^^^3), since the value of A() is determined by what S can prove, not by what “common sense” can prove.
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.)
It does imply that. What happens is that you (in “common sense” system) don’t prove A()=2 as a consequence of proving (say) both (A()=1 ⇒ U()=1000000) and (A()=2 ⇒ U()=3^^^3), since the value of A() is determined by what S can prove, not by what “common sense” can prove.
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.)