the list of Examples (here) was essentially empty. I have now !include
d foundational axiom - contents.
the term ‘logical framework’, which I think is what we want there.
We were having a related discussion here.
]]>Slight edits, including explicitly using the term ‘logical framework’, which I think is what we want there.
The most significant edit is that I generalised the example sequent to have lists for antecedent and succedent. This made reading the following text a little confusing, so I made the example show only one sequent. (The text still says a collection of sequents like the one in the example.)
]]>Yeah, pretty much I think. I made “deductive system” point to logical framework.
]]>Okay, thanks. We have that entry logical framework which maybe might serve to wrap up that list of possibilities. But I am not really sure.
]]>Of course I agree with that, and I made some changes to reflect this. See what you think now.
]]>Thanks. Given the recent discussion about sequent calculus, I am wondering: where it currently says “in a sequent calculus” should we more precisely say “in a sequent calculus or in a system of natural deduction”?
]]>Edited the definition at the article axiom.
]]>