Skip to main content
Changed title in view of a simpler case added
Link

Characterize pairs Two simple cases of elements in aquantifier elimination for Heyting algebra having form $(q\lor\neg q,q'\lor\neg q')$ with $q\land q'=\bot$algebras

added a simpler case
Source Link

This extracts a simple case from a cross-post at cs.SE.

Here is a fact about Intuitionistic Propositional Logic:

A formula $p$ is equivalent to a formula of the form $q \lor \neg q$ if and only if $\neg p$ is false.

This can be reformulated in algebraic semantics:

For any Heyting algebra $H$ and any element $p\in H$, there exists a $q\in H$ with $p=q\lor\neg q$ if and only if $\neg p=\bot$ (the bottom element of $H$).

This eliminates an existential quantifier, in the sense of finding an equivalent condition on $p$ which does not involve any "there exists" statement.

This leads to the question that interests me:

Given a pair of elements $p,p'$ in a Heyting algebra $H$, when can they be written as $p=q\lor\neg q$ and $p'=q'\lor\neg q'$ with $q\land q'=\bot$?

Is it possible to eliminate existential quantifiers here too?

Much later -- update: a still simpler similar question which I also do not know anything about.

Can one eliminate the existential quantifier from the following formula (in the language of Heyting algebras): $$ \exists x\ p = (q\land x)\lor\neg(q\land x) $$

This extracts a simple case from a cross-post at cs.SE.

Here is a fact about Intuitionistic Propositional Logic:

A formula $p$ is equivalent to a formula of the form $q \lor \neg q$ if and only if $\neg p$ is false.

This can be reformulated in algebraic semantics:

For any Heyting algebra $H$ and any element $p\in H$, there exists a $q\in H$ with $p=q\lor\neg q$ if and only if $\neg p=\bot$ (the bottom element of $H$).

This eliminates an existential quantifier, in the sense of finding an equivalent condition on $p$ which does not involve any "there exists" statement.

This leads to the question that interests me:

Given a pair of elements $p,p'$ in a Heyting algebra $H$, when can they be written as $p=q\lor\neg q$ and $p'=q'\lor\neg q'$ with $q\land q'=\bot$?

Is it possible to eliminate existential quantifiers here too?

This extracts a simple case from a cross-post at cs.SE.

Here is a fact about Intuitionistic Propositional Logic:

A formula $p$ is equivalent to a formula of the form $q \lor \neg q$ if and only if $\neg p$ is false.

This can be reformulated in algebraic semantics:

For any Heyting algebra $H$ and any element $p\in H$, there exists a $q\in H$ with $p=q\lor\neg q$ if and only if $\neg p=\bot$ (the bottom element of $H$).

This eliminates an existential quantifier, in the sense of finding an equivalent condition on $p$ which does not involve any "there exists" statement.

This leads to the question that interests me:

Given a pair of elements $p,p'$ in a Heyting algebra $H$, when can they be written as $p=q\lor\neg q$ and $p'=q'\lor\neg q'$ with $q\land q'=\bot$?

Is it possible to eliminate existential quantifiers here too?

Much later -- update: a still simpler similar question which I also do not know anything about.

Can one eliminate the existential quantifier from the following formula (in the language of Heyting algebras): $$ \exists x\ p = (q\land x)\lor\neg(q\land x) $$

the abbreviation is never used
Source Link

This extracts a simple case from a cross-post at cs.SE.

Here is a fact about Intuitionistic Propositional Logic (IPL):

A formula $p$ is equivalent to a formula of the form $q \lor \neg q$ if and only if $\neg p$ is false.

This can be reformulated in algebraic semantics:

For any Heyting algebra $H$ and any element $p\in H$, there exists a $q\in H$ with $p=q\lor\neg q$ if and only if $\neg p=\bot$ (the bottom element of $H$).

This eliminates an existential quantifier, in the sense of finding an equivalent condition on $p$ which does not involve any "there exists" statement.

This leads to the question that interests me:

Given a pair of elements $p,p'$ in a Heyting algebra $H$, when can they be written as $p=q\lor\neg q$ and $p'=q'\lor\neg q'$ with $q\land q'=\bot$?

Is it possible to eliminate existential quantifiers here too?

This extracts a simple case from a cross-post at cs.SE.

Here is a fact about Intuitionistic Propositional Logic (IPL):

A formula $p$ is equivalent to a formula of the form $q \lor \neg q$ if and only if $\neg p$ is false.

This can be reformulated in algebraic semantics:

For any Heyting algebra $H$ and any element $p\in H$, there exists a $q\in H$ with $p=q\lor\neg q$ if and only if $\neg p=\bot$ (the bottom element of $H$).

This eliminates an existential quantifier, in the sense of finding an equivalent condition on $p$ which does not involve any "there exists" statement.

This leads to the question that interests me:

Given a pair of elements $p,p'$ in a Heyting algebra $H$, when can they be written as $p=q\lor\neg q$ and $p'=q'\lor\neg q'$ with $q\land q'=\bot$?

Is it possible to eliminate existential quantifiers here too?

This extracts a simple case from a cross-post at cs.SE.

Here is a fact about Intuitionistic Propositional Logic:

A formula $p$ is equivalent to a formula of the form $q \lor \neg q$ if and only if $\neg p$ is false.

This can be reformulated in algebraic semantics:

For any Heyting algebra $H$ and any element $p\in H$, there exists a $q\in H$ with $p=q\lor\neg q$ if and only if $\neg p=\bot$ (the bottom element of $H$).

This eliminates an existential quantifier, in the sense of finding an equivalent condition on $p$ which does not involve any "there exists" statement.

This leads to the question that interests me:

Given a pair of elements $p,p'$ in a Heyting algebra $H$, when can they be written as $p=q\lor\neg q$ and $p'=q'\lor\neg q'$ with $q\land q'=\bot$?

Is it possible to eliminate existential quantifiers here too?

no arithmetic is mentioned anywhere in the question
Link
Emil Jeřábek
  • 47.2k
  • 4
  • 147
  • 208
Loading
edited tags
Link
YCor
  • 63.9k
  • 5
  • 187
  • 286
Loading
Tried another title
Link
Loading
deleted 23 characters in body
Source Link
Andrej Bauer
  • 48.8k
  • 11
  • 131
  • 239
Loading
streamlined
Source Link
user44143
user44143
Loading
highlighted the question
Source Link
Loading
highlighted the question
Source Link
Loading
Loading