構文論的方法
違いは真偽値を使うかどうか
いまいち分からないな
構文論的方法の場合、何が正しい（真）/正しくない（偽）とかが無い、という事かな
仮に「公理」っていう真っぽいものを定義するとしても、それは真でも偽でもなく、「公理」でしかない
記号の連なりを記号の連なりとして捉えて機械的に処理することで数学をする、みたいな理解（今のところ）
これはプログラムっぽいのでfamiliarな印象
数学のミニチュアモデルの「形式的体系H」を作る、ってのをやってる
すげ〜〜
記号IMPLY: $ (x)→(y) を $ \neg(x)\lor(y)と定義する
プログラムでいうところのエイリアスとかwrapperみたいな物かな
意味が解釈される事なく文字列としてそのまま置き換えられるっていう感じだと、C++のusingとかが近そう
ただ、なんでこういう定義をしてるのかいまいち分からんな
形式的体系を扱う時にそれは考えなくて良いんだろうけど、理解するなら裏にある意図も掴みたい
意味論的に考えるなら「aならばb」の真偽が「 not a または b」の真偽と一致するってことかな
でも意味わからん
「りんごが美味しい ならば アップルパイも美味しい」で考えると、
りんごが美味しい & アップルパイが美味しい: true
りんごが美味しい & アップルパイがまずい: false
りんごがまずい & アップルパイが美味しい: true
りんごがまずい & アップルパイがまずい: true
「aならばb」のaが偽な時点でなんでもOK、みたいな感じなのかな
ギリ納得できそう
形式的体系では、定義された文字列の操作を機械的に実行していくだけで、意味論でいう「推論」のような事が行える