Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
at decidable proposition I found the simple basic idea a bit too deeply hidden in the text. In an attempt to improve on this I have added right before the subsections of the Idea-section this quick preview:
External decidability: either $p$ or $\not p$ may be deduced in the metalanguage;
Internal decidability: $p \vee \not p$ may be deduced, hence “$p$ or not $p$” holds in the object language.
Okay?
I tried to clarify a little.
1 to 2 of 2