# Does a formula denote it's truth value once the variable is assigned?

In a lot of systems like boolean algebra '=' is treated as a function that takes two inputs and yields a truth value.

In first-order logic we often use an expression like 1. p(x)=(x+1=2) and to treat 'x+1=2' as something that can denote a truth value when assigned to it makes sense that both P 'x' and and formula 1 are elements of the object language.

Can we take that in most systems with binary relations, that if 'xRy' is true for a relation R for x,y' that xRy denotes a specific truth value?

`P(x)` is an expression of the object language. Everything else - assignments of variables, interpretations of predicates/relations, truth values and the equivalence sign between formal symbols and their denotation - is part of the meta language.

Once we assigned a value to `x` (such as `1`), and fixed an interpretation for `P` (such as "let `P` be that property such that `P(x)` holds iff `x + 1 = 2`), we can say that the formula `P(x)` denotes the truth value `1`, and typically write this as `[[P(x)]]^M,g = 1`.

Okay, Lemontree's answer is spot on.

In a lot of systems like boolean algebra '=' is treated as a function.

There is a function f(x)=x, but it might be better to consider the sign '=' as an identity relation rather reflecting on the identity function. The difference is that in the identity relation, we bring to the fore three important concepts: symmetry, reflexivity, and transitivity and the notion that '=' captures a domain mapping onto itself.

Now, as to your real question, what it seems to me is you're asking about what can and can't be done in a formal system. You ask:

Can we take that in most systems with binary relations, that if 'xRy' is true for a relation R for x,y' that xRy=1 where '1' denotes true?

What I read this as is 'can we presume that a formal system that assigns a truth value to a proposition in a calculus use 1 and 0 for true and false?' That's an empirical quesiton, so I can only speak anecdotally on the matter.

From my experience the answer is that it all depends on the person inventing the formal system. Is it normal to do so? I think it's discipline specific. In mathematics, I don't think most systems used in argumentation are defined that way, though obviously in Boolean and Heyting Algebras it is done that way. A mathematician would better able to speak to mathematical formal systems. I WOULD say in computer science, its rather routine to make 1 and the boolean type 'true' equivalent in evaluation of statements (propostions) in loosely typed formalisms. There are formalisms that actually do the opposite. They define 0 as false, and any other integer or real value as true. It's handy when working with types to use Boolean expressions to evalute arithmetic results.

What's important to take away is that anything at all can be done in an object language described by a metalanguage, and that programming languages implemented by formal systems are different than formal systems used by logicians to explore logic and different still from the formal systems used by mathematicians to prove theorems. On the whole, I suspect that other than as a syntactic sugar for coders, there isn't much advantage. I was looking at WP's entry on Heyting algebras and they have the Heyting formal system, but then talk in terms of intuitionistic logic and present propositions in the form 'p(x)=T' instead of 'p(x)=1', so I suspect that the latter sort of statement enjoys limited use in the wider formal systems of mathematics and logic, though I'd be happy to be proven wrong to know with certainty!