I have heard of judgments, entails, usual implies, was just wondering what small subset I actually need to create my own (sort of) type theory (it's a block / arrows app I'm writing).
When do you use entails over usual implies? Is judgement just a notational thing, i.e. you draw a horizontal line and write above and below it for the hypothesis and conclusion respectively. If it is just notational, then would you convert it to a usual implies or to an entailment?
More specifically, observe the following diagram:
What should the three subscripted $\text{?}$'s be? I.e. what type of implication. And lastly what should I call the grouping of two type statements for use in the hypothesis of a judgement? It's the node at the bottom and currently says "Judgement Hypotheses".
Clearly, logical "or" is handled by natural branching of arrows. So grouping of the type statements would be inhabitation of what type, or do I just color the node differently and call it logical "and"?
The diagram is basically a way to go from type theory to diagram rendering (my app's specialty) using a visual language that specifies what to do. The language derives its expressive power from the known power of type theory. A node is nested in a parent node precisely when that parent node is a type and the nested node is an inhabitant. But perhaps it could mean other things as well. Not sure!
When working with logic, we are proving theorems about how we prove theorems, and so it is important to separate the "meta-logic", which is how we as mathematicians in the outside world reason about thing, from the "inner-logic", which is how somebody using only the tools inside the logic we are studying would reason.
Judgements define how the inner-logic behaves, and gives us as meta-mathematicians tools for proving that, say, "every inner-logic-provable statement is true of all its models". Judgements turn the inner-logic into a mathematical gadget like any other, which we can reason about. There's no real need for the new notation, involving proof trees and horizontal lines. We do it (in part) to make the separation between inner and meta logic clear to the reader (Some authors don't do this. It makes reading the paper a nightmare, though.).
Regular Implication, then, is something done inside the logic of study. It is the tool that someone living inside the inner-logic would use to prove things, blissfully unaware of the meta-mathematical tools which lie beyond their reach.
The confusion is made worse because we as humans know how logic should work, and so we often try to make our inner-logic behave in a similar way to our meta-logic. For instance, we almost always include a rule like the following:
This rule tells us how to prove (in the meta-language) that $A \to B$ is provable in the inner-language. $A \to B$ is provable (in the inner-language) whenever we can prove $B$ using $A$ an additional assumption (again, in the inner-language).
This article talks about judgements, and is both good and short. This book might also clarify things by putting judgements in a more general light - it discusses programming languages, and how to formalize them as logics (with type theory). It's a bit long, but if you only read the first few chapters you might see another way of thinking about how judgements (in the meta logic) correspond to properties which are provable (in the inner logic).
I hope this helps ^_^