Judgements of the kind we are considering here were first introduced by Frege in his Begriffsscrift.
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 an expression
to make an asserted judgement.
(in Frege this is the combination of
"|", asserting and "-" forming a judgement but the pair have since been
treated as a single symbol)
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.