jcreed@andrejbauer @boarders @maxsnew ok that all sounds agreeable... but is there a concrete example I can chew on where "infinite conjunction" disagrees with "universal quantification"? I think that's where my grip on which definitions are being used is weak
Andrej Bauer*Internally* ∀ agrees with infima (which is what you probably mean by "infinite conjunction") because that is what the inference rules for ∀ state.
*Externally* there is a difference. Consider Peano arithmetic (PA) and a statement ¬Prf(n, ⌜0=1⌝) stating that n does not encode a PA-proof of 0=1. The statement ∀n.¬Prf(n,⌜0=1⌝) is not probable in PA, as it says that PA is consitent. However, the statements
¬Prf(0, ⌜0=1⌝)
¬Prf(1, ⌜0=1⌝)
¬Prf(2, ⌜0=1⌝)
¬Prf(3, ⌜0=1⌝)
...
are all provable in PA, therefore their infimum is true.
CubeRootOfTrue