diff --git a/ql/src/codeql/GlobalValueNumbering.qll b/ql/src/codeql/GlobalValueNumbering.qll
new file mode 100644
index 00000000000..e9b4728a6be
--- /dev/null
+++ b/ql/src/codeql/GlobalValueNumbering.qll
@@ -0,0 +1,244 @@
+private import ql
+private import codeql_ql.ast.internal.Predicate
+private import codeql_ql.ast.internal.Type
+private import codeql_ql.ast.internal.Builtins
+
+private newtype TValueNumber =
+  TVariableValueNumber(VarDecl var) { variableAccessValueNumber(_, var) } or
+  TFieldValueNumber(VarDecl var) { fieldAccessValueNumber(_, var) } or
+  TThisValueNumber(Predicate pred) { thisAccessValueNumber(_, pred) } or
+  TPredicateValueNumber(PredicateOrBuiltin pred, ValueNumberArgumentList args) {
+    predicateCallValueNumber(_, pred, args)
+  } or
+  TClassPredicateValueNumber(PredicateOrBuiltin pred, ValueNumber base, ValueNumberArgumentList args) {
+    classPredicateCallValueNumber(_, pred, base, args)
+  } or
+  TLiteralValueNumber(string value, Type t) { literalValueNumber(_, value, t) } or
+  TBinaryOpValueNumber(FunctionSymbol symbol, ValueNumber leftOperand, ValueNumber rightOperand) {
+    binaryOperandValueNumber(_, symbol, leftOperand, rightOperand)
+  } or
+  TUnaryOpValueNumber(FunctionSymbol symbol, ValueNumber operand) {
+    unaryOperandValueNumber(_, symbol, operand)
+  } or
+  TInlineCastValueNumber(ValueNumber operand, Type t) { inlineCastValueNumber(_, operand, t) } or
+  TDontCareValueNumber() or
+  TRangeValueNumber(ValueNumber lower, ValueNumber high) { rangeValueNumber(_, lower, high) } or
+  TSetValueNumber(ValueNumberElementList elements) { setValueNumber(_, elements) } or
+  TUniqueValueNumber(Expr e) { uniqueValueNumber(e) }
+
+private newtype ValueNumberArgumentList =
+  MkArgsNil() or
+  MkArgsCons(ValueNumber head, ValueNumberArgumentList tail) {
+    argumentValueNumbers(_, _, head, tail)
+  }
+
+private newtype ValueNumberElementList =
+  MkElementsNil() or
+  MkElementsCons(ValueNumber head, ValueNumberElementList tail) {
+    setValueNumbers(_, _, head, tail)
+  }
+
+private ValueNumberArgumentList argumentValueNumbers(Call call, int start) {
+  start = call.getNumberOfArguments() and
+  result = MkArgsNil()
+  or
+  exists(ValueNumber head, ValueNumberArgumentList tail |
+    argumentValueNumbers(call, start, head, tail) and
+    result = MkArgsCons(head, tail)
+  )
+}
+
+private predicate argumentValueNumbers(
+  Call call, int start, ValueNumber head, ValueNumberArgumentList tail
+) {
+  head = valueNumber(call.getArgument(start)) and
+  tail = argumentValueNumbers(call, start + 1)
+}
+
+private ValueNumberElementList setValueNumbers(Set set, int start) {
+  start = set.getNumberOfElements() and
+  result = MkElementsNil()
+  or
+  exists(ValueNumber head, ValueNumberElementList tail |
+    setValueNumbers(set, start, head, tail) and
+    result = MkElementsCons(head, tail)
+  )
+}
+
+private predicate setValueNumbers(Set set, int start, ValueNumber head, ValueNumberElementList tail) {
+  head = valueNumber(set.getElement(start)) and
+  tail = setValueNumbers(set, start + 1)
+}
+
+/**
+ * A value number. A value number represents a collection of expressions that compute to the same value
+ * at runtime.
+ */
+class ValueNumber extends TValueNumber {
+  string toString() { result = "GVN" }
+
+  /** Gets an expression that has this value number. */
+  final Expr getAnExpr() { this = valueNumber(result) }
+}
+
+private predicate uniqueValueNumber(Expr e) { not numberable(e) }
+
+private predicate numberable(Expr e) {
+  e instanceof VarAccess or
+  e instanceof FieldAccess or
+  e instanceof ThisAccess or
+  e instanceof Call or
+  e instanceof Literal or
+  e instanceof BinOpExpr or
+  e instanceof UnaryExpr or
+  e instanceof InlineCast or
+  e instanceof ExprAnnotation or
+  e instanceof DontCare or
+  e instanceof Range or
+  e instanceof Set or
+  e instanceof AsExpr
+}
+
+private predicate variableAccessValueNumber(VarAccess access, VarDef var) {
+  access.getDeclaration() = var
+}
+
+private predicate fieldAccessValueNumber(FieldAccess access, VarDef var) {
+  access.getDeclaration() = var
+}
+
+private predicate thisAccessValueNumber(ThisAccess access, Predicate pred) {
+  access.getEnclosingPredicate() = pred
+}
+
+private predicate predicateCallValueNumber(
+  Call call, PredicateOrBuiltin pred, ValueNumberArgumentList args
+) {
+  call.getTarget() = pred and
+  not exists(call.(MemberCall).getBase()) and
+  args = argumentValueNumbers(call, 0)
+}
+
+private predicate classPredicateCallValueNumber(
+  MemberCall call, PredicateOrBuiltin pred, ValueNumber base, ValueNumberArgumentList args
+) {
+  call.getTarget() = pred and
+  valueNumber(call.getBase()) = base and
+  args = argumentValueNumbers(call, 0)
+}
+
+private predicate literalValueNumber(Literal lit, string value, Type t) {
+  lit.(String).getValue() = value and
+  t instanceof StringClass
+  or
+  lit.(Integer).getValue().toString() = value and
+  t instanceof IntClass
+  or
+  lit.(Float).getValue().toString() = value and
+  t instanceof FloatClass
+  or
+  lit.(Boolean).isFalse() and
+  value = "false" and
+  t instanceof BooleanClass
+  or
+  lit.(Boolean).isTrue() and
+  value = "true" and
+  t instanceof BooleanClass
+}
+
+private predicate binaryOperandValueNumber(
+  BinOpExpr e, FunctionSymbol symbol, ValueNumber leftOperand, ValueNumber rightOperand
+) {
+  e.getOperator() = symbol and
+  valueNumber(e.getLeftOperand()) = leftOperand and
+  valueNumber(e.getRightOperand()) = rightOperand
+}
+
+private predicate unaryOperandValueNumber(UnaryExpr e, FunctionSymbol symbol, ValueNumber operand) {
+  e.getOperator() = symbol and
+  valueNumber(e.getOperand()) = operand
+}
+
+private predicate inlineCastValueNumber(InlineCast cast, ValueNumber operand, Type t) {
+  valueNumber(cast.getBase()) = operand and
+  cast.getTypeExpr().getResolvedType() = t
+}
+
+private predicate rangeValueNumber(Range range, ValueNumber lower, ValueNumber high) {
+  valueNumber(range.getLowEndpoint()) = lower and
+  valueNumber(range.getHighEndpoint()) = high
+}
+
+private predicate setValueNumber(Set set, ValueNumberElementList elements) {
+  elements = setValueNumbers(set, 0)
+}
+
+private TValueNumber nonUniqueValueNumber(Expr e) {
+  exists(VarDecl var |
+    variableAccessValueNumber(e, var) and
+    result = TVariableValueNumber(var)
+  )
+  or
+  exists(VarDecl var |
+    fieldAccessValueNumber(e, var) and
+    result = TFieldValueNumber(var)
+  )
+  or
+  exists(Predicate pred |
+    thisAccessValueNumber(e, pred) and
+    result = TThisValueNumber(pred)
+  )
+  or
+  exists(PredicateOrBuiltin pred, ValueNumberArgumentList args |
+    predicateCallValueNumber(e, pred, args) and
+    result = TPredicateValueNumber(pred, args)
+  )
+  or
+  exists(PredicateOrBuiltin pred, ValueNumber base, ValueNumberArgumentList args |
+    classPredicateCallValueNumber(e, pred, base, args) and
+    result = TClassPredicateValueNumber(pred, base, args)
+  )
+  or
+  exists(string value, Type t |
+    literalValueNumber(e, value, t) and
+    result = TLiteralValueNumber(value, t)
+  )
+  or
+  exists(FunctionSymbol symbol, ValueNumber leftOperand, ValueNumber rightOperand |
+    binaryOperandValueNumber(e, symbol, leftOperand, rightOperand) and
+    result = TBinaryOpValueNumber(symbol, leftOperand, rightOperand)
+  )
+  or
+  exists(FunctionSymbol symbol, ValueNumber operand |
+    unaryOperandValueNumber(e, symbol, operand) and
+    result = TUnaryOpValueNumber(symbol, operand)
+  )
+  or
+  exists(ValueNumber operand, Type t |
+    inlineCastValueNumber(e, operand, t) and
+    result = TInlineCastValueNumber(operand, t)
+  )
+  or
+  result = valueNumber([e.(ExprAnnotation).getExpression(), e.(AsExpr).getInnerExpr()])
+  or
+  e instanceof DontCare and result = TDontCareValueNumber()
+  or
+  exists(ValueNumber lower, ValueNumber high |
+    rangeValueNumber(e, lower, high) and
+    result = TRangeValueNumber(lower, high)
+  )
+  or
+  exists(ValueNumberElementList elements |
+    setValueNumber(e, elements) and
+    result = TSetValueNumber(elements)
+  )
+}
+
+/** Gets the value number of an expression `e`. */
+cached
+TValueNumber valueNumber(Expr e) {
+  result = nonUniqueValueNumber(e)
+  or
+  uniqueValueNumber(e) and
+  result = TUniqueValueNumber(e)
+}
diff --git a/ql/src/codeql_ql/ast/Ast.qll b/ql/src/codeql_ql/ast/Ast.qll
index c207672bfd3..920bc757cfa 100644
--- a/ql/src/codeql_ql/ast/Ast.qll
+++ b/ql/src/codeql_ql/ast/Ast.qll
@@ -816,6 +816,9 @@ class Call extends TCall, Expr, Formula {
     none() // overriden in sublcasses.
   }
 
+  /** Gets an argument of this call, if any. */
+  final Expr getAnArgument() { result = getArgument(_) }
+
   PredicateOrBuiltin getTarget() { resolveCall(this, result) }
 
   override Type getType() { result = this.getTarget().getReturnType() }
@@ -1791,7 +1794,19 @@ class FunctionSymbol extends string {
 /**
  * A binary operation expression, such as `x + 3` or `y / 2`.
  */
-class BinOpExpr extends TBinOpExpr, Expr { }
+class BinOpExpr extends TBinOpExpr, Expr {
+  /** Gets the left operand of the binary expression. */
+  Expr getLeftOperand() { none() } // overriden in subclasses
+
+  /* Gets the right operand of the binary expression. */
+  Expr getRightOperand() { none() } // overriden in subclasses
+
+  /** Gets the operator of the binary expression. */
+  FunctionSymbol getOperator() { none() } // overriden in subclasses
+
+  /* Gets an operand of the binary expression. */
+  final Expr getAnOperand() { result = getLeftOperand() or result = getRightOperand() }
+}
 
 /**
  * An addition or subtraction expression.
@@ -1802,17 +1817,11 @@ class AddSubExpr extends TAddSubExpr, BinOpExpr {
 
   AddSubExpr() { this = TAddSubExpr(expr) and operator = expr.getChild().getValue() }
 
-  /** Gets the left operand of the binary expression. */
-  Expr getLeftOperand() { toGenerated(result) = expr.getLeft() }
+  override Expr getLeftOperand() { toGenerated(result) = expr.getLeft() }
 
-  /* Gets the right operand of the binary expression. */
-  Expr getRightOperand() { toGenerated(result) = expr.getRight() }
+  override Expr getRightOperand() { toGenerated(result) = expr.getRight() }
 
-  /* Gets an operand of the binary expression. */
-  Expr getAnOperand() { result = getLeftOperand() or result = getRightOperand() }
-
-  /** Gets the operator of the binary expression. */
-  FunctionSymbol getOperator() { result = operator }
+  override FunctionSymbol getOperator() { result = operator }
 
   override PrimitiveType getType() {
     // Both operands are the same type
@@ -1872,16 +1881,12 @@ class MulDivModExpr extends TMulDivModExpr, BinOpExpr {
   MulDivModExpr() { this = TMulDivModExpr(expr) and operator = expr.getChild().getValue() }
 
   /** Gets the left operand of the binary expression. */
-  Expr getLeftOperand() { toGenerated(result) = expr.getLeft() }
+  override Expr getLeftOperand() { toGenerated(result) = expr.getLeft() }
 
   /** Gets the right operand of the binary expression. */
-  Expr getRightOperand() { toGenerated(result) = expr.getRight() }
+  override Expr getRightOperand() { toGenerated(result) = expr.getRight() }
 
-  /** Gets an operand of the binary expression. */
-  Expr getAnOperand() { result = getLeftOperand() or result = getRightOperand() }
-
-  /** Gets the operator of the binary expression. */
-  FunctionSymbol getOperator() { result = operator }
+  override FunctionSymbol getOperator() { result = operator }
 
   override PrimitiveType getType() {
     // Both operands are of the same type
@@ -1954,6 +1959,11 @@ class Range extends TRange, Expr {
    */
   Expr getHighEndpoint() { toGenerated(result) = range.getUpper() }
 
+  /**
+   * Gets the lower and upper bounds of the range.
+   */
+  Expr getAnEndpoint() { result = [getLowEndpoint(), getHighEndpoint()] }
+
   override PrimitiveType getType() { result.getName() = "int" }
 
   override string getAPrimaryQlClass() { result = "Range" }
@@ -1980,6 +1990,16 @@ class Set extends TSet, Expr {
    */
   Expr getElement(int i) { toGenerated(result) = set.getChild(i) }
 
+  /**
+   * Gets an element in this set literal expression, if any.
+   */
+  Expr getAnElement() { result = getElement(_) }
+
+  /**
+   * Gets the number of elements in this set literal expression.
+   */
+  int getNumberOfElements() { result = count(getAnElement()) }
+
   override Type getType() { result = this.getElement(0).getType() }
 
   override string getAPrimaryQlClass() { result = "Set" }
diff --git a/ql/src/codeql_ql/ast/internal/Builtins.qll b/ql/src/codeql_ql/ast/internal/Builtins.qll
index 072bb8299f2..9e1d45d5242 100644
--- a/ql/src/codeql_ql/ast/internal/Builtins.qll
+++ b/ql/src/codeql_ql/ast/internal/Builtins.qll
@@ -65,3 +65,18 @@ string getArgType(string args, int i) { result = args.splitAt(",", i).trim() }
 class StringClass extends PrimitiveType {
   StringClass() { this.getName() = "string" }
 }
+
+/** The primitive 'int' class. */
+class IntClass extends PrimitiveType {
+  IntClass() { this.getName() = "int" }
+}
+
+/** The primitive 'float' class. */
+class FloatClass extends PrimitiveType {
+  FloatClass() { this.getName() = "float" }
+}
+
+/** The primitive 'boolean' class. */
+class BooleanClass extends PrimitiveType {
+  BooleanClass() { this.getName() = "boolean" }
+}
diff --git a/ql/src/queries/style/SuperfluousExists.ql b/ql/src/queries/style/SuperfluousExists.ql
new file mode 100644
index 00000000000..40a6c4054fd
--- /dev/null
+++ b/ql/src/queries/style/SuperfluousExists.ql
@@ -0,0 +1,99 @@
+/**
+ * @name Superfluous 'exists' conjunct.
+ * @description Writing 'exists(x)' when the existence of X is implied by another conjunct is bad practice.
+ * @kind problem
+ * @problem.severity warning
+ * @precision high
+ * @id ql/superfluous-exists
+ * @tags maintainability
+ */
+
+import ql
+import codeql.GlobalValueNumbering
+
+/**
+ * Gets an operand of this conjunction (we need the restriction
+ * to `Conjunction` to get the correct transitive closure).
+ */
+Formula getAConjOperand(Conjunction conj) { result = conj.getAnOperand() }
+
+/** A conjunction that is not a operand of another conjunction. */
+class TopLevelConjunction extends Conjunction {
+  TopLevelConjunction() { not this = getAConjOperand(_) }
+
+  /** Gets a formula within this conjunction that is not itself a conjunction. */
+  Formula getAnAtom() {
+    not result instanceof Conjunction and
+    result = getAConjOperand*(this)
+  }
+}
+
+/**
+ * Holds if the existence of `e` implies the existence of `vn`. For instance, the existence of
+ * `1 + x` implies the existence of a value number `vn` such that `vn.getAnExpr() = x`.
+ */
+predicate exprImpliesExists(ValueNumber vn, Expr e) {
+  vn.getAnExpr() = e
+  or
+  exprImpliesExists(vn, e.(BinOpExpr).getAnOperand())
+  or
+  exprImpliesExists(vn, e.(InlineCast).getBase())
+  or
+  exprImpliesExists(vn, e.(PredicateCall).getAnArgument())
+  or
+  exprImpliesExists(vn, [e.(MemberCall).getAnArgument(), e.(MemberCall).getBase()])
+  or
+  exprImpliesExists(vn, e.(UnaryExpr).getOperand())
+  or
+  exprImpliesExists(vn, e.(ExprAnnotation).getExpression())
+  or
+  forex(Formula child | child = e.(Set).getAnElement() | exprImpliesExists(vn, child))
+  or
+  exprImpliesExists(vn, e.(AsExpr).getInnerExpr())
+  or
+  exprImpliesExists(vn, e.(Range).getAnEndpoint())
+  or
+  exists(ExprAggregate agg |
+    agg = e and
+    agg.getKind().matches(["strict%", "unique"]) and
+    exprImpliesExists(vn, agg.getExpr(0))
+  )
+}
+
+/**
+ * Holds if the satisfiability of `f` implies the existence of `vn`. For instance, if `x.foo()` is
+ * satisfied, the value number `vn` such that `vn.getAnExpr() = x` exists.
+ */
+predicate formulaImpliesExists(ValueNumber vn, Formula f) {
+  forex(Formula child | child = f.(Disjunction).getAnOperand() | formulaImpliesExists(vn, child))
+  or
+  formulaImpliesExists(vn, f.(Conjunction).getAnOperand())
+  or
+  exprImpliesExists(vn, f.(ComparisonFormula).getAnOperand())
+  or
+  exists(IfFormula ifFormula | ifFormula = f |
+    exprImpliesExists(vn, ifFormula.getCondition())
+    or
+    formulaImpliesExists(vn, ifFormula.getThenPart()) and
+    formulaImpliesExists(vn, ifFormula.getElsePart())
+  )
+  or
+  exprImpliesExists(vn, f.(InstanceOf).getExpr())
+  or
+  exprImpliesExists(vn, f.(PredicateCall).getAnArgument())
+  or
+  exprImpliesExists(vn, [f.(MemberCall).getAnArgument(), f.(MemberCall).getBase()])
+  or
+  exists(InFormula inFormula | inFormula = f |
+    exprImpliesExists(vn, [inFormula.getExpr(), inFormula.getRange()])
+  )
+}
+
+from TopLevelConjunction toplevel, Exists existsFormula, ValueNumber vn, Formula conjunct
+where
+  existsFormula = toplevel.getAnAtom() and
+  vn.getAnExpr() = existsFormula.getExpr() and
+  conjunct = toplevel.getAnAtom() and
+  formulaImpliesExists(vn, conjunct)
+select existsFormula, "This conjunct is superfluous as the existence is implied by $@.", conjunct,
+  "this conjunct"