# Logical negation in Prolog ~ a = (a =\> f)

**URL:** <https://swi-prolog.discourse.group/t/logical-negation-in-prolog-a-a-f/9253>\
**Category:** Data Structure\
**Tags:** how-to\
**Created:** [September 7, 2025, 2:54pm UTC](https://swi-prolog.discourse.group/t/logical-negation-in-prolog-a-a-f/9253 "2025-09-07T14:54:12Z")\
**Posts on this page:** 2\
**Page:** 1

<div class="post-metadata">

**Author:** ![joseph-vidal-rosset](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/joseph-vidal-rosset/32/2594_2.png) [@joseph-vidal-rosset](https://swi-prolog.discourse.group/u/joseph-vidal-rosset)\
**Post date:** [September 7, 2025, 2:54pm UTC](https://swi-prolog.discourse.group/t/logical-negation-in-prolog-a-a-f/9253/1 "2025-09-07T14:54:12Z")

</div>

```prolog
% =========================================================================
% TPTP Operators 
% =========================================================================
:- op( 500, fy, ~). % negation
:- op(1000, xfy, &). % conjunction
:- op(1100, xfy, '|'). % disjunction
:- op(1110, xfy, =>). % conditional
:- op(1120, xfy, <=>). % biconditional
:- op( 500, fy, !). % universal quantifier: ![X]:
:- op( 500, fy, ?). % existential quantifier: ?[X]:
:- op( 500, xfy, :). % quantifier separator

```

With the previous operators, it would be useful for a Prolog program to read any ~ a as (a =\> f) with f meaning falsum or bot. So:

```prolog
term_expansion(~ ~ A, Result) :-
    !,
    expand_negations(A, A1),
    Result = ((A1 => f) => f).

term_expansion(~ A, Result) :-
    !,
    expand_negations(A, A1),
    Result = (A1 => f).

expand_negations(~ ~ A, ((A1 => f) => f)) :-
    !,
    expand_negations(A, A1).

expand_negations(~ A, (A1 => f)) :-
    !,
    expand_negations(A, A1).

expand_negations((A | B), (A1 | B1)) :-
    !,
    expand_negations(A, A1),
    expand_negations(B, B1).

expand_negations((A & B), (A1 & B1)) :-
    !,
    expand_negations(A, A1),
    expand_negations(B, B1).

expand_negations((A => B), (A1 => B1)) :-
    !,
    expand_negations(A, A1),
    expand_negations(B, B1).

expand_negations(A, A) :-
    atomic(A).

```

But :

```prolog
 ?- term_expansion(~ ~ (~ a | a), X).
X = (((a=>f)| a=>f)=>f).

?- term_expansion(~ (~ (~ a | a)), X).
X = (((a=>f)| a=>f)=>f).

```

are clearly wrong .

A solution would be helpful.

Best wishes,  
Jo.

---

<div class="post-metadata">

**Author:** ![joseph-vidal-rosset](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/joseph-vidal-rosset/32/2594_2.png) [@joseph-vidal-rosset](https://swi-prolog.discourse.group/u/joseph-vidal-rosset)\
**Post date:** [September 7, 2025, 4:06pm UTC](https://swi-prolog.discourse.group/t/logical-negation-in-prolog-a-a-f/9253/3 "2025-09-07T16:06:25Z")

</div>

Hi, you are right. But it is a kind of “display bug” . I had a Prolog file to show the problem . And I consider that my perplexity was understandable, but you gave the explanation. SWI-Prolog shoud correct this to get the solution. 🙂

[demo\_bug.pl](https://swi-prolog.discourse.group/uploads/short-url/3Aex7La439CATqr1Bd4uKnIfYrG.pl) (1,4 Ko)