# Tag Info

5

The $x$ in $\forall x . P(x)$ is not an argument. It is a bound variable indicating which variable the quantifer is ranging over. Let us compare the situation to the definite integral, for concretness just from $0$ to $1$. Here is an example: $$\int_0^1 x^2 + 3 x \, dx$$ This is a very archaic way of writing mathematical expressions that mathematicians like ...

4

One answer is that we use English, but that's not what you're looking for. To make the question more precise, let us ask what sort of formalism is useful for describing logics. This is still quite broad, because a logic has several parts: syntax, rules of inference, semantics, etc. Syntax is pretty well understood and we know that the syntax of a language ...

3

The theory of higher-order critical pairs can indeed handle this example, as outlined in the following article: Higher-Order Rewrite Systems and their Confluence, Richard Mayr & Tobias Nipkow There are several different notions of higher-order rewrite systems, and several of them are able to handle your example, including those of the paper. The ...

2

Generally you have: Some boolean variables that collectively represent the current state, say $s,t,u$. Some boolean variables that collectively represents the inputs, say $i,j,k$. For instance, you might have one variable per sensor (assuming each sensor returns a boolean value). Some boolean variables that collectively represents the inputs, say $o,p,q$. ...

2

As you may know, "interesting" classes of language often correspond to "interesting" classes of automata and also "interesting" algebras. For example, regular languages correspond to NFAs/DFAs, and Kleene algebras. It's the same with logic. Interesting logics often corresponding to interesting category structures, interesting programming languages, and so ...

Only top voted, non community-wiki answers of a minimum length are eligible