**"Imaginary" meets and joins?**

Dealing with meets and joins seems to require peppering the discussion with annoying qualifiers, "if the meet exists." I was wondering if there was a way to do things more loosely.

In the early days of real algebra, polynomial roots sometimes existed, and sometimes didn't, such as for \\(x^2+1=0\\). Then they tried just asserting that a solution exists, and got the imaginary numbers.

At first, they thought of the imaginaries as only "scaffolding", which were used on the way to a solution, but couldn't be part of the final answer. Have folks found it useful to do something similar with meets and joins? Just assert that they all exist, by augmenting the preorder with new "imaginary" elements \\(\boxed\top\\) and \\(\boxed\bot\\) that are greater/less than the entire preorder.

A formula such as

$$(a \wedge b) \vee a = a$$

seems like a "reasonable" identity, because we don't care what the meet is, just the fact that it must be less than \\(a\\). But it fails to evaluate when the meet doesn't exist, even though we're not even going to look at it. The identity feels like it should be "locally" true no matter what the "global" structure of the preorder is. By permitting it to formally resolve to \\(\boxed\bot\\ \vee a = a\\) whenever necessary, the identity evaluates to true for all preorders.

There may be terrible pitfalls with this approach, so I'm curious whether it's something that has been explored and found useful?

Dealing with meets and joins seems to require peppering the discussion with annoying qualifiers, "if the meet exists." I was wondering if there was a way to do things more loosely.

In the early days of real algebra, polynomial roots sometimes existed, and sometimes didn't, such as for \\(x^2+1=0\\). Then they tried just asserting that a solution exists, and got the imaginary numbers.

At first, they thought of the imaginaries as only "scaffolding", which were used on the way to a solution, but couldn't be part of the final answer. Have folks found it useful to do something similar with meets and joins? Just assert that they all exist, by augmenting the preorder with new "imaginary" elements \\(\boxed\top\\) and \\(\boxed\bot\\) that are greater/less than the entire preorder.

A formula such as

$$(a \wedge b) \vee a = a$$

seems like a "reasonable" identity, because we don't care what the meet is, just the fact that it must be less than \\(a\\). But it fails to evaluate when the meet doesn't exist, even though we're not even going to look at it. The identity feels like it should be "locally" true no matter what the "global" structure of the preorder is. By permitting it to formally resolve to \\(\boxed\bot\\ \vee a = a\\) whenever necessary, the identity evaluates to true for all preorders.

There may be terrible pitfalls with this approach, so I'm curious whether it's something that has been explored and found useful?