A frozen FOL

36 views

Skip to first unread message

fl

unread,

Mar 14, 2020, 10:32:34 AM3/14/20

to meta...@googlegroups.com

I think it would be good to have a file with the FOL theorems isolated and frozen. By "frozen" I mean that the list of axioms, theorems, proofs, symbols and identifiers would never be changed again. This file would contain only the theorems actually in use and could be a basis for other studies different from FOL + ZFC. I think I should write FOL + equality to be exact. There was at least one precedent for this. Knuth had found it necessary to freeze the sgb-words file of the 5757 five-letter words of the English language.