rzach/forallx-yyc

make FOL be an extension of TFL

Closed this issue · 2 comments

rzach commented

Allow zero-place predicates (these would naturally symbolize sentences like "it's raining"). It somehow seems more elegant to me if FOL keeps everything from TFL but just allows for more logical structure to be revealed. I don't think this would require many changes. The syntax in 26.2 is already consistent with it. For the semantics, you could just have interpretations include valuations. Maybe this makes the notion of an interpretation a bit less natural, though...

rzach commented

Suggested by @ettta

rzach commented

Fixed with commit b790acc