Frege's Judgements
Judgements of the kind we are considering here were first introduced by Frege in his Begriffscrift.
In ordinary language writing or uttering a sentence is normally understood as asserting it, and special measures are necessary to mention a sentence without asserting it (e.g. enclosing it in quotation marks), Frege chose to reverse the defaults for his formal notation, using the symbol " " to be used in front of a sentence to make an asserted judgement.
|
|
Hilbert's Metanotation
Hilbert introduced the field of metamathematics, in which mathematical methods were applied to the study of formal mathematical notations.
This involved the use of two languages, an object language being studied, and a meta-language in which claims about the object language are expressed.
" " was then pressed into service as metanotation.
" p" asserts the provability of p in the object logic, "p q" asserts (in the metalanguage) that q is derivable from p in the object logic.
|
|
Judgements in Object Language
Possibly because of their convenience as a means for controlling the structure of proofs, judgement forms are now part of the object language in most formal logical systems.
The forms of judgement chosen are important in the pragmatics of describing and constructing formal proofs in the object logic, or may influence the ease with which the metatheory can be developed.
|
|